const ordinal : set prop const SNo_ : set set prop const Subq : set set prop axiom SNoLev_uniq_Subq: !x:set.!y:set.!z:set.ordinal y -> ordinal z -> SNo_ y x -> SNo_ z x -> Subq y z axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y claim !x:set.!y:set.!z:set.ordinal y -> ordinal z -> SNo_ y x -> SNo_ z x -> y = z