# Strict Lower Closure of Sum with One

## Theorem

Let $\left({S, \circ, \preceq}\right)$ be a naturally ordered semigroup.

Then:

$\forall n \in \left({S, \circ, \preceq}\right): \left({n \circ 1}\right)^\prec = n^\prec \cup \left\{{n}\right\}$

where $n^\prec$ is defined as the strict lower closure of $n$, that is, the set of elements strictly preceding $n$.

## Proof

First note that as $\left({S, \circ, \preceq}\right)$ is well-ordered and hence totally ordered, the Trichotomy Law applies.

Thus:

 $\displaystyle \forall m \in S:$  $\displaystyle m \notin n^\prec$ $\displaystyle$ $\iff$ $\displaystyle \neg \ m \prec n$ Definition of Strict Lower Closure $\displaystyle$ $\iff$ $\displaystyle m = n \lor n \prec m$ Trichotomy Law $\displaystyle$ $\iff$ $\displaystyle n \preceq m$ Definition of Strictly Precede

So:

 $\displaystyle \forall p \in S:$  $\displaystyle p \notin \left({n \circ 1}\right)^\prec$ $\displaystyle$ $\iff$ $\displaystyle n \circ 1 \preceq p$ from the above $\displaystyle$ $\iff$ $\displaystyle n \prec p$ Sum with One is Immediate Successor in Naturally Ordered Semigroup

Similarly:

 $\displaystyle \forall p \in S:$  $\displaystyle p \notin n^\prec \cup \left\{ {n}\right\}$ $\displaystyle$ $\iff$ $\displaystyle n \preceq p \land n \ne p$ from the above $\displaystyle$ $\iff$ $\displaystyle n \prec p$ Definition of Strictly Precede

So:

$p \notin n^\prec \cup \left\{{n}\right\} \iff p \notin \left({n \circ 1}\right)^\prec$

Thus:

$\complement_S \left({\left({n \circ 1}\right)^\prec}\right) = \complement_S \left({n^\prec \cup \left\{{n}\right\}}\right)$

from the definition of relative complement.

So:

 $\displaystyle \left({n \circ 1}\right)^\prec$ $=$ $\displaystyle \complement_S \left({\complement_S \left({\left({n \circ 1}\right)^\prec}\right)}\right)$ Relative Complement of Relative Complement $\displaystyle$ $=$ $\displaystyle \complement_S \left({\complement_S \left({n^\prec \cup \left\{ {n}\right\} }\right)}\right)$ from above $\displaystyle$ $=$ $\displaystyle n^\prec \cup \left\{ {n}\right\}$ Relative Complement of Relative Complement

$\blacksquare$