Let $\mathbb{N}$ be the D225: Set of natural numbers such that

(i)	$x^+$ is a D589: Successor set of $x$ for any $x \in \mathbb{N}$

A D554: Binary operation $+ : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ is a basic natural number addition operation if and only if

(1)	\begin{equation} \forall \, n \in \mathbb{N} : n + 0 = n \end{equation}
(2)	\begin{equation} \forall \, n, m \in \mathbb{N} : n + m^+ = (n + m)^+ \end{equation}