# Strict Lower Closure of Sum with One

## Theorem

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.

Then:

$\forall n \in \struct {S, \circ, \preceq}: \paren {n \circ 1}^\prec = n^\prec \cup \set n$

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 $\struct {S, \circ, \preceq}$ is well-ordered and hence totally ordered, the Trichotomy Law applies.

Thus:

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

So:

 $\ds \forall p \in S: \,$ $\ds$  $\ds p \notin \paren {n \circ 1}^\prec$ $\ds$ $\leadstoandfrom$ $\ds n \circ 1 \preceq p$ from the above $\ds$ $\leadstoandfrom$ $\ds n \prec p$ Sum with One is Immediate Successor in Naturally Ordered Semigroup

Similarly:

 $\ds \forall p \in S: \,$ $\ds$  $\ds p \notin n^\prec \cup \set n$ $\ds$ $\leadstoandfrom$ $\ds n \preceq p \land n \ne p$ from the above $\ds$ $\leadstoandfrom$ $\ds n \prec p$ Definition of Strictly Precede

So:

$p \notin n^\prec \cup \set n \iff p \notin \paren {n \circ 1}^\prec$

Thus:

$\relcomp S {\paren {n \circ 1}^\prec} = \relcomp S {n^\prec \cup \set n}$

from the definition of relative complement.

So:

 $\ds \paren {n \circ 1}^\prec$ $=$ $\ds \relcomp S {\relcomp S {\paren {n \circ 1}^\prec} }$ Relative Complement of Relative Complement $\ds$ $=$ $\ds \relcomp S {\relcomp S {n^\prec \cup \set n} }$ from above $\ds$ $=$ $\ds n^\prec \cup \set n$ Relative Complement of Relative Complement

$\blacksquare$