Definition. onat_inductive_sets_eq
onat_inductive_sets = {A | ∅ ∈ A ∧ ∀n. n ∈ A → n ∪ {n} ∈ A}