Way Below implies Preceding

Theorem

Let $\left({S, \preceq}\right)$ be an ordered set.

Let $x, y \in S$ such that

$x \ll y$

where $\ll$ denotes element is way below second element.

Then

$x \preceq y$

Proof

By Singleton is Directed and Filtered Subset:

$\left\{ {y}\right\}$ is directed.

By Supremum of Singleton:

$\left\{ {y}\right\}$ admits a supremum and $\sup \left\{ {y}\right\} = y$

By definition of reflexivity:

$y \preceq \sup \left\{ {y}\right\}$

By definition of way below:

$\exists d \in \left\{ {y}\right\}: x \preceq d$

Thus by definition of singleton:

$x \preceq y$

$\blacksquare$

Sources

• 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices

• Mizar article WAYBEL_3:1