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