const ordinal : set prop const SNo_ : set set prop const SNo : set prop axiom SNo_SNo: !x:set.ordinal x -> !y:set.SNo_ x y -> SNo y 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 -> !y:set.SNo_ x y -> SNoLev y = x