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 term nIn = \x:set.\y:set.~ x iIn y const omega : set term finite = \x:set.?y:set.y iIn omega & equip x y const Repl : set (set set) set axiom ReplI: !x:set.!f:set set.!y:set.y iIn x -> f y iIn Repl x f const SNo : set prop const minus_SNo : set set term - = minus_SNo axiom minus_SNo_invol: !x:set.SNo x -> - - x = x axiom ReplE_impred: !x:set.!f:set set.!y:set.y iIn Repl x f -> !P:prop.(!z:set.z iIn x -> y = f z -> P) -> P 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 axiom equip_sym: !x:set.!y:set.equip x y -> equip y x axiom equip_tra: !x:set.!y:set.!z:set.equip x y -> equip y z -> equip x z const Empty : set const SNo_min_of : set set prop lemma !x:set.(!y:set.y iIn x -> SNo y) -> finite x -> x != Empty -> (!y:set.y iIn Repl x minus_SNo -> SNo y) -> finite (Repl x minus_SNo) -> ?y:set.SNo_min_of x y var x:set hyp !y:set.y iIn x -> SNo y hyp finite x hyp x != Empty claim (!y:set.y iIn Repl x minus_SNo -> SNo y) -> ?y:set.SNo_min_of x y