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.