const SNo : set prop const ordinal : set prop const SNoLev : set set axiom SNoLev_ordinal: !x:set.SNo x -> ordinal (SNoLev x) const ordsucc : set set axiom ordinal_ordsucc: !x:set.ordinal x -> ordinal (ordsucc x) const SNo_ : set set prop const SNo_extend1 : set set axiom SNo_extend1_SNo_: !x:set.SNo x -> SNo_ (ordsucc (SNoLev x)) (SNo_extend1 x) axiom SNoLev_uniq2: !x:set.ordinal x -> !y:set.SNo_ x y -> SNoLev y = x claim !x:set.SNo x -> SNoLev (SNo_extend1 x) = ordsucc (SNoLev x)