Strict Lower Closure is Lower Section/Proof 1

Theorem

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

Let $p \in S$.

Let $p^\prec$ denote the strict lower closure of $p$.

Then $p^\prec$ is a lower section.

Proof

Let $l \in p^\prec$.

Let $s \in S$ with $s \preceq l$.

Then by the definition of strict lower closure:

$l \prec p$

Thus by Extended Transitivity:

$s \prec p$

So by the definition of strict lower closure:

$s \in p^\prec$

Since this holds for all such $l$ and $s$, $p^\prec$ is a lower section.

$\blacksquare$