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