The well-ordering principle

Suppose $S$ is nonempty but has no least element.

If $m<\sigma (n)$ then $m\le n$: by [L2] applied to $m$ and $\sigma (n)$ we get $\sigma (m)\le \sigma (n)$, say $\sigma (m)+i=\sigma (n)$; then $\sigma (m+i)=\sigma (m)+i=\sigma (n)$ [L5], so $m+i=n$ by injectivity [L4], hence $m\le n$.

First, $0\in T$: if $0\in S$ then $0\le s$ for all $s\in S$, since $0+s=s$ [L6], making $0$ a least element, contrary to the assumption; hence $0\mathrm{\notin }S$; moreover $m\le 0$ forces $m=0$, because $m\mathrm{\ne }0$ would give $0<m$ (as $0+m=m$ [L6] with $m\mathrm{\ne }0$) while $m\le 0$ gives $m<0$, and [L3] admits at most one of these; so every $m\le 0$ lies outside $S$.

Next, $T$ is closed under $\sigma$: assume $n\in T$; if $\sigma (n)\in S$ then no $s\in S$ satisfies $s<\sigma (n)$ (else $s\le n$ by step 1.2, so $s\mathrm{\notin }S$ because $n\in T$, a contradiction), hence $\sigma (n)\le s$ for all $s\in S$ by [L3], making $\sigma (n)$ a least element, contrary to the assumption; therefore $\sigma (n)\mathrm{\notin }S$, and any $m$ with $m\le \sigma (n)$ satisfies $m=\sigma (n)$ or $m\mathrm{\ne }\sigma (n)$; in the second case $m\le \sigma (n)$ together with $m\mathrm{\ne }\sigma (n)$ gives $m<\sigma (n)$ by the definition of the strict order, hence $m\le n$ by step 1.2 and $m\mathrm{\notin }S$ because $n\in T$, while in the first case $m=\sigma (n)\mathrm{\notin }S$; so every $m\le \sigma (n)$ lies outside $S$, giving $\sigma (n)\in T$.

By the induction principle [L1], from $0\in T$ and closure under $\sigma$, $T=\mathbb{N}$; then for every $n$, taking $m=n\le n$ shows $n\mathrm{\notin }S$, so $S=\mathrm{\varnothing }$, contradicting nonemptiness; therefore $S$ has a least element.