Lemma 1.8.2.1.  Let m, n ∈ , f: ℕ<m ↔ ℕ<n be a bijection. Then:
m = n
No proof.
Remarks.

This lemma is part of the well-definedness proof of the embedding of the natural numbers into the cardinal numbers.