const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term nIn = \x:set.\y:set.~ x iIn y const ordsucc : set set axiom ordsuccI1: !x:set.Subq x (ordsucc x) var x:set var f:set set var y:set var z:set var w:set hyp !u:set.u iIn ordsucc (ordsucc x) -> !v:set.v iIn ordsucc (ordsucc x) -> f u = f v -> u = v hyp z iIn ordsucc (ordsucc x) hyp ordsucc w iIn ordsucc (ordsucc x) hyp ~ Subq y z hyp Subq y w hyp f z = f (ordsucc w) claim z != ordsucc w