const ordinal : set prop const ordsucc : set set axiom ordinal_ordsucc: !x:set.ordinal x -> ordinal (ordsucc x) const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const SNo : set prop const SNoLev : set set lemma !p:set prop.!x:set.(!y:set.ordinal y -> !z:set.z iIn SNoS_ y -> p z) -> SNo x -> ordinal (SNoLev x) -> ordinal (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 claim ordinal (SNoLev x) -> p x