const nat_p : set prop const ordsucc : set set const Empty : set axiom nat_1: nat_p (ordsucc Empty) 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 SNo (ordsucc Empty)