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