const SNo : set prop const SNoLev : set set const minus_SNo : set set term - = minus_SNo axiom minus_SNo_Lev: !x:set.SNo x -> SNoLev - x = SNoLev x const ordinal : set prop const In : set set prop term iIn = In infix iIn 2000 2000 const ordsucc : set set const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 lemma !x:set.!y:set.ordinal x -> SNo y -> SNoLev y iIn ordsucc x -> SNo - y -> SNoLev - y iIn ordsucc x -> - x <= y var x:set var y:set hyp ordinal x hyp SNo y hyp SNoLev y iIn ordsucc x claim SNo - y -> - x <= y