Lower Closure of Singleton

Theorem

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

Let $s$ be an element of $S$.

Then:

$\set s^\preceq = s^\preceq$

where:

$\set s^\preceq$ denotes the lower closure of $\set s$

$s^\preceq$ denotes the lower closure of $s$.

Proof

\(\ds \set s^\preceq\)

\(=\)

\(\ds \bigcup \set {t^\preceq: t \in \set s}\)

Definition of Lower Closure of Subset

\(\ds \)

\(=\)

\(\ds \bigcup \set {s^\preceq}\)

Definition of Singleton

\(\ds \)

\(=\)

\(\ds s^\preceq\)

Union of Singleton

$\blacksquare$

Sources

• Mizar article WAYBEL_0:def 17