const bij : set set (set set) prop term equip = \x:set.\y:set.?f:set set.bij x y f const In : set set prop term iIn = In infix iIn 2000 2000 const omega : set term finite = \x:set.?y:set.y iIn omega & equip x y term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term nIn = \x:set.\y:set.~ x iIn y const binunion : set set set axiom binunionI1: !x:set.!y:set.!z:set.z iIn x -> z iIn binunion x y const Sing : set set axiom SingI: !x:set.x iIn Sing x axiom binunionI2: !x:set.!y:set.!z:set.z iIn y -> z iIn binunion x y const ordsucc : set set axiom ordsuccE: !x:set.!y:set.y iIn ordsucc x -> y iIn x | y = x axiom FalseE: ~ False axiom ordsuccI1: !x:set.Subq x (ordsucc x) axiom ordsuccI2: !x:set.x iIn ordsucc x axiom SingE: !x:set.!y:set.y iIn Sing x -> y = x axiom binunionE: !x:set.!y:set.!z:set.z iIn binunion x y -> z iIn x | z iIn y axiom bijI: !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) -> bij x y f var x:set var y:set var z:set var f:set set hyp !w:set.w iIn z -> f w iIn x hyp !w:set.w iIn z -> !u:set.u iIn z -> f w = f u -> w = u hyp !w:set.w iIn x -> ?u:set.u iIn z & f u = w hyp nIn y x claim (?f2:set set.(!w:set.w iIn z -> f2 w = f w) & f2 z = y) -> ?f2:set set.bij (ordsucc z) (binunion x (Sing y)) f2