Way Above Closure is Subset of Upper Closure of Element

Theorem

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

Let $x \in S$.

Then:

$x^\gg \subseteq x^\succeq$

where

$x^\gg$ denotes the way above closure of $x$

$x^\succeq$ denotes the upper closure of $x$.

Proof

Let $y \in x^\gg$.

By definition of way above closure:

$x \ll y$

where $\ll$ denotes the way below relation.

By Way Below implies Preceding:

$x \preceq y$

Thus by definition of upper closure of element:

$y \in x^\succeq$

$\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:11