const SNo : set prop const ordinal : set prop const SNoLev : set set const SNo_ : set set prop axiom SNoLev_prop: !x:set.SNo x -> ordinal (SNoLev x) & SNo_ (SNoLev x) x claim !x:set.SNo x -> ordinal (SNoLev x)