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 SNoR : set set axiom ordinal_SNoR: !x:set.ordinal x -> SNoR x = Empty claim SNoR (ordsucc Empty) = Empty