Supremum in Ordered Subset

Theorem

Let $L = \struct {S, \preceq}$ be an ordered set.

Let $R = \struct {T, \preceq'}$ be an ordered subset of $L$.

Let $X \subseteq T$ such that

$X$ admits an supremum in $L$.

Then $\sup_L X \in T$ if and only if

$X$ admits an supremum in $R$ and $\sup_R X = \sup_L X$

Proof

This follows by mutatis mutandis of the proof of Infimum in Ordered Subset.

$\blacksquare$

Sources

• Mizar article YELLOW_0:64