Definition. onat_eq
onat = ⋂{A | ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A}
The natural numbers, represented as the first
ordinal numbers. The number zero is the empty set, the
successor operation is succ. The inherent induction
principle is shown by onat_induction_sets and
onat_induction.