const SNo : set prop const ordinal : set prop const SNoLev : set set axiom SNoLev_ordinal: !x:set.SNo x -> ordinal (SNoLev x) const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNo_max_SNoLev: !x:set.SNo x -> (!y:set.y iIn SNoS_ (SNoLev x) -> y < x) -> SNoLev x = x claim !x:set.SNo x -> (!y:set.y iIn SNoS_ (SNoLev x) -> y < x) -> ordinal x