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