const ordinal : set prop const SNo_ : set set prop term SNo = \x:set.?y:set.ordinal y & SNo_ y x axiom ordinal_SNo_: !x:set.ordinal x -> SNo_ x x claim !x:set.ordinal x -> ?y:set.ordinal y & SNo_ y x