Order completeness (source code)

= Order completeness

= Order-complete
{synonym}

Every nonempty bounded-above subset of a <total order> has a least upper bound. In the real line this is the <supremum> property used to extend maps defined on an <order-dense subset>.