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_extend0 : set set axiom SNo_extend0_SNo_: !x:set.SNo x -> SNo_ (ordsucc (SNoLev x)) (SNo_extend0 x) axiom SNo_SNo: !x:set.ordinal x -> !y:set.SNo_ x y -> SNo y claim !x:set.SNo x -> SNo (SNo_extend0 x)