const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term TransSet = \x:set.!y:set.y iIn x -> Subq y x const ordinal : set prop const omega : set axiom omega_ordinal: ordinal omega const SNo : set prop const SNo_ : set set prop const SNoLev : set set axiom SNoLev_: !x:set.SNo x -> SNo_ (SNoLev x) x const SNoS_ : set set axiom SNoS_I: !x:set.ordinal x -> !y:set.!z:set.z iIn x -> SNo_ z y -> y iIn SNoS_ x const ordsucc : set set var x:set var y:set hyp SNo y hyp SNoLev y iIn SNoLev x hyp SNoLev x iIn ordsucc omega claim SNoLev y iIn omega -> y iIn SNoS_ omega