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 lemma !p:set prop.!x:set.(!y:set.ordinal y -> !z:set.z iIn SNoS_ y -> p z) -> SNo x -> ordinal (ordsucc (SNoLev x)) -> x iIn SNoS_ (ordsucc (SNoLev x)) -> p x var p:set prop var x:set hyp !y:set.ordinal y -> !z:set.z iIn SNoS_ y -> p z hyp SNo x hyp ordinal (SNoLev x) claim ordinal (ordsucc (SNoLev x)) -> p x