Lower Closures are Equal implies Elements are Equal

Theorem

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

Let $x, y \in S$ such that

$x^\preceq = y^\preceq$

where $x^\preceq$ denotes the lower closure of $x$.

Then $x = y$

Proof

By definitions of lower closure of element and reflexivity:

$x \in x^\preceq$ and $y \in y^\preceq$

By definition of lower closure of element:

$x \preceq y$ and $y \preceq x$

Thus by definition of antisymmetry:

$x = y$

$\blacksquare$

Sources

• Mizar article WAYBEL_0:19