Definition 1.8.1.22.2.  Let n ∈ . We define:
n:= {m ∈  : m ≤ n} = <(n+1)
Equality.  No proof.