Way Above Closure is Upper

Theorem

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

Let $x \in S$.

Then $x^\gg$ is upper

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

Proof

Let $y \in x^\gg$, $z \in S$ such that

$y \preceq z$

By definition of way above closure:

$x \ll y$

By Preceding and Way Below implies Way Below:

$x \ll z$

Thus by definition of way above closure:

$z \in x^\gg$

$\blacksquare$

Sources

• Mizar article WAYBEL_3:funcreg 3