const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const ordsucc : set set axiom ordsuccI2: !x:set.x iIn ordsucc x const ordinal : set prop const SNo : set prop const SNoLev : set set const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom ordinal_SNoLev_max_2: !x:set.ordinal x -> !y:set.SNo y -> SNoLev y iIn ordsucc x -> y <= x const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoLtLe_tra: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x < y -> y <= z -> x < z const omega : set var x:set var y:set hyp SNo x hyp SNo y hyp x < y hyp SNoLev y iIn omega hyp ordinal (SNoLev y) claim SNo (SNoLev y) -> ?z:set.z iIn omega & x < z