const ordsucc : set set const Empty : set axiom neq_ordsucc_0: !x:set.ordsucc x != Empty claim ordsucc (ordsucc Empty) != Empty