const Empty : set const ordsucc : set set axiom neq_0_1: Empty != ordsucc Empty axiom ordsucc_inj_contra: !x:set.!y:set.x != y -> ordsucc x != ordsucc y claim ordsucc Empty != ordsucc (ordsucc Empty)