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