\begin{definition}[Definition:Integer/Formal Definition]
Let $\struct {\N, +}$ be the commutative semigroup of natural numbers under addition.
From Inverse Completion of Natural Numbers, we can create $\struct {\N', +'}$, an inverse completion of $\struct {\N, +}$.
From Construction of Inverse Completion, this is done as follows:
Let $\boxtimes$ be the cross-relation defined on $\N \times \N$ by:
:$\tuple {x_1, y_1} \boxtimes \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$
From Cross-Relation is Congruence Relation, $\boxtimes$ is a congruence relation.
Let $\struct {\N \times \N, \oplus}$ be the external direct product of $\struct {\N, +}$ with itself, where $\oplus$ is the operation on $\N \times \N$ induced by $+$ on $\N$:
:$\tuple {x_1, y_1} \oplus \tuple {x_2, y_2} = \tuple {x_1 + x_2, y_1 + y_2}$
Let the quotient structure defined by $\boxtimes$ be $\struct {\dfrac {\N \times \N} \boxtimes, \oplus_\boxtimes}$
where $\oplus_\boxtimes$ is the operation induced on $\dfrac {\N \times \N} \boxtimes$ by $\oplus$.
Let us use $\N'$ to denote the quotient set $\dfrac {\N \times \N} \boxtimes$.
Let us use $+'$ to denote the operation $\oplus_\boxtimes$.
Thus $\struct {\N', +'}$ is the Inverse Completion of Natural Numbers.
As the Inverse Completion is Unique up to isomorphism, it follows that we can ''define'' the structure $\struct {\Z, +}$ which is isomorphic to $\struct {\N', +'}$.
An element of $\N'$ is therefore an equivalence class of the congruence relation $\boxtimes$.
So an element of $\Z$ is the isomorphic image of an element $\eqclass {\tuple {a, b} } \boxtimes$ of $\dfrac {\N \times \N} \boxtimes$.
The set of elements $\Z$ is called '''the integers'''.
\end{definition}