const SNo : set prop const minus_SNo : set set term - = minus_SNo axiom SNo_minus_SNo: !x:set.SNo x -> SNo - x const ordinal : set prop 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 lemma !x:set.!y:set.ordinal x -> SNo y -> SNoLev y iIn ordsucc x -> SNo - y -> - x <= y claim !x:set.ordinal x -> !y:set.SNo y -> SNoLev y iIn ordsucc x -> - x <= y