Dedekind completion
= Dedekind completion
{c}
The completion of a <total order> by its nonprincipal proper cuts, supplying least upper bounds. For a dense order it contains the original order densely, and preserves the interval countable chain condition and separability or nonseparability.