const SNo : set prop const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const ordsucc : set set const SNoLev : set set axiom SNoS_SNoLev: !x:set.SNo x -> x iIn SNoS_ (ordsucc (SNoLev x)) const ordinal : set prop const Subq : set set prop const minus_SNo : set set term - = minus_SNo lemma !x:set.SNo x -> ordinal (ordsucc (SNoLev x)) -> x iIn SNoS_ (ordsucc (SNoLev x)) -> Subq (SNoLev - x) (SNoLev x) var x:set hyp SNo x hyp ordinal (SNoLev x) claim ordinal (ordsucc (SNoLev x)) -> Subq (SNoLev - x) (SNoLev x)