Preceding implies if Less Upper Bound then Greater Upper Bound

Theorem

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

Let $x, y \in S$ such that

$x \preceq y$

Let $X \subseteq S$.

Then

$x$ is upper bound for $X \implies y$ is upper bound for $X$

and

$y$ is lower bound for $X \implies x$ is lower bound for $X$.

Proof

First Implication

Let $x$ be upper bound for $X$,

Let $z \in X$.

By definition of upper bound:

$z \preceq x$

Thus by definition of transitivity:

$z \preceq y$

$\Box$

Second Implication

This follows by mutatis mutandis.

$\blacksquare$

Sources

• Mizar article YELLOW_0:4