const In : set set prop term iIn = In infix iIn 2000 2000 term bij = \x:set.\y:set.\f:set set.(!z:set.z iIn x -> f z iIn y) & (!z:set.z iIn x -> !w:set.w iIn x -> f z = f w -> z = w) & !z:set.z iIn y -> ?w:set.w iIn x & f w = z const If_i : prop set set set axiom If_i_0: !P:prop.!x:set.!y:set.~ P -> If_i P x y = y axiom If_i_1: !P:prop.!x:set.!y:set.P -> If_i P x y = x axiom xm: !P:prop.P | ~ P const ordsucc : set set var x:set var f:set set var y:set var z:set var w:set hyp !u:set.u iIn x -> !v:set.v iIn x -> f u = f v -> u = v hyp ~ ?u:set.u iIn x & f u = y hyp w iIn ordsucc x hyp z != x -> z iIn x claim (w != x -> w iIn x) -> If_i (z = x) y (f z) = If_i (w = x) y (f w) -> z = w