Rewrite the first two Peano axioms in
Section Peano-section as a single axiom that defines
${NatNum}(x)$ so as to exclude the possibility of natural numbers
except for those generated by the successor function.
Rewrite the first two Peano axioms in Section Peano-section as a single axiom that defines ${NatNum}(x)$ so as to exclude the possibility of natural numbers except for those generated by the successor function.