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