const ordinal : set prop const Empty : set axiom ordinal_Empty: ordinal Empty const SNo : set prop axiom ordinal_SNo: !x:set.ordinal x -> SNo x claim SNo Empty