216
[1Z1]Prerequisites:[1Z0]. (Proposed on 2023-01-17)
Suppose \(X\) has no maximum; let \(S\) be defined as in [1Z0]; show that is an injective function
\[ S:X→ X\quad , \]
and that \(S(x)≠ 0_ X\), for every \(x\) (that is, \(0_ X\) is not successor of any element).
1
We note that in general \(S\) will not be surjective, as a function \(S: X→ X⧵ \{ 0_ X\} \): there may be elements \(y∈ S, y≠ 0_ X\) that are not successors of an element. If, however, for a given \(y∈ X\), there exists \(x∈ X\) such that \(y=S(x)\), we will say that \(x\) is the predecessor of \(y\).