const nat_p : set prop const ordinal : set prop axiom nat_p_ordinal: !x:set.nat_p x -> ordinal x const SNo : set prop axiom ordinal_SNo: !x:set.ordinal x -> SNo x claim !x:set.nat_p x -> SNo x