const ordinal : set prop const SNo : set prop axiom ordinal_SNo: !x:set.ordinal x -> SNo x const SNo_ : set set prop axiom ordinal_SNo_: !x:set.ordinal x -> SNo_ x x axiom SNoLev_uniq: !x:set.!y:set.!z:set.ordinal y -> ordinal z -> SNo_ y x -> SNo_ z x -> y = z const SNoLev : set set axiom SNoLev_prop: !x:set.SNo x -> ordinal (SNoLev x) & SNo_ (SNoLev x) x claim !x:set.ordinal x -> SNoLev x = x