const ordinal : set prop const SNo : set prop axiom ordinal_SNo: !x:set.ordinal x -> SNo x const In : set set prop term iIn = In infix iIn 2000 2000 const SNoLev : set set const ordsucc : 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 minus_SNo : set set term - = minus_SNo axiom minus_SNo_Le_contra: !x:set.!y:set.SNo x -> SNo y -> x <= y -> - y <= - x axiom minus_SNo_invol: !x:set.SNo x -> - - x = x var x:set var y:set hyp ordinal x hyp SNo y hyp SNoLev y iIn ordsucc x hyp SNo - y claim SNoLev - y iIn ordsucc x -> - x <= y