const In : set set prop term iIn = In infix iIn 2000 2000 const ordsucc : set set axiom ordsuccI2: !x:set.x iIn ordsucc x axiom ordsuccE: !x:set.!y:set.y iIn ordsucc x -> y iIn x | y = x lemma !x:set.!y:set.ordsucc x = ordsucc y -> x iIn y -> y iIn ordsucc x -> x = y var x:set var y:set hyp ordsucc x = ordsucc y claim x iIn ordsucc y -> x = y