N#DEF. Natural Numbers / Finite Ordinals.
We define
\[\N = \bigcap\{X:\text{$X$ is inductive}\}.\]Axiom of Infinity guarantees the existence of at least one inductive set.
$\omega:=\N$ is an ordinal. When treating $\N$ as a set, the symbol $\N$ is used. When treating it as an ordinal, the symbol $\omega$ is used.
$n$ is a natural number / finite ordinal if $n\in\N$.
An ordinal is infinite if it is not finite.
We define
\[0=\varnothing, \quad 1=0+1, \quad 2=1+1, \quad 3=2+1\]and so on.
$\omega$ is the least limit ordinal.
Proof.By LO#PROP-E (I) $\lrimp$ (V).