const ordinal : set prop const omega : set axiom omega_ordinal: ordinal omega const In : set set prop term iIn = In infix iIn 2000 2000 const ordsucc : set set axiom omega_ordsucc: !x:set.x iIn omega -> ordsucc x iIn omega const Subq : set set prop const SNoS_ : set set const SNoCutP : set set prop const SNoLev : set set const SNoCut : set set set axiom SNoCutP_SNoCut_lim: !x:set.ordinal x -> (!y:set.y iIn x -> ordsucc y iIn x) -> !y:set.Subq y (SNoS_ x) -> !z:set.Subq z (SNoS_ x) -> SNoCutP y z -> SNoLev (SNoCut y z) iIn ordsucc x claim !x:set.Subq x (SNoS_ omega) -> !y:set.Subq y (SNoS_ omega) -> SNoCutP x y -> SNoLev (SNoCut x y) iIn ordsucc omega