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 SNo_ : set set prop lemma !x:set.!y:set.SNo y -> SNoLev y = x -> SNoLev - y = x -> SNo_ x - y const ordinal : set prop var x:set var y:set hyp ordinal x hyp SNo_ x y hyp SNo y claim SNoLev y = x -> SNo_ x - y