Definition 1.8.1.45.  Let m, n ∈ . We define:
max(m, n) := max({m, n}) = {m if m ≥ nn if m < n = {m if n = 0({n if m = 0max(x, y) + 1 if m = x + 1 (x ∈ )) if n = y + 1 (y ∈ )
Equality.  No proof.
References.