const Empty : set const ordsucc : set set axiom neq_0_ordsucc: !x:set.Empty != ordsucc x axiom neq_i_sym: !x:set.!y:set.x != y -> y != x claim !x:set.ordsucc x != Empty