Preceding implies Way Below Closure is Subset of Way Below Closure

Theorem

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

Let $x, y \in S$ such that

$x \preceq y$

Then $x^\ll \subseteq y^\ll$

where $x^\ll$ denotes the way below closure of $x$.

Proof

Let $z \in x^\ll$.

By definition of way below closure:

$z \ll x$

By Preceding and Way Below implies Way Below and definition of reflexivity:

$z \ll y$

Thus by definition of way below closure:

$z \in y^\ll$

$\blacksquare$

Sources

• Mizar article WAYBEL_3:12