\begin{definition}[Definition:Non-Successor Element]
Let $\struct {P, s, 0}$ be a Peano structure.
Then the element $0 \in P$ is called the '''non-successor element'''.
This is justified by {{PeanoAxiom|4}}, which stipulates that $0$ is not in the image of the successor mapping $s$.
\end{definition}