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 SNo : set prop const minus_SNo : set set term - = minus_SNo axiom SNo_minus_SNo: !x:set.SNo x -> SNo - x const Repl : set (set set) set 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 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) -> ?y:set.SNo_min_of x y claim !x:set.(!y:set.y iIn x -> SNo y) -> finite x -> x != Empty -> ?y:set.SNo_min_of x y