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 axiom ordsuccI2: !x:set.x iIn ordsucc x const SNo_ : set set prop 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 SNo : set prop const SNoLev : set set axiom SNoLev_prop: !x:set.SNo x -> ordinal (SNoLev x) & SNo_ (SNoLev x) x claim !x:set.SNo x -> x iIn SNoS_ (ordsucc (SNoLev x))