const ordinal : set prop const omega : set axiom omega_ordinal: ordinal omega const SNo : set prop axiom ordinal_SNo: !x:set.ordinal x -> SNo x claim SNo omega