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 SNo_max_of : set set prop const Repl : set (set set) set const minus_SNo : set set term - = minus_SNo const SNo_min_of : set set prop axiom minus_SNo_max_min': !x:set.!y:set.(!z:set.z iIn x -> SNo z) -> SNo_max_of (Repl x minus_SNo) y -> SNo_min_of x - y const Empty : set axiom finite_max_exists: !x:set.(!y:set.y iIn x -> SNo y) -> finite x -> x != Empty -> ?y:set.SNo_max_of x y var x:set hyp !y:set.y iIn x -> SNo y hyp x != Empty hyp !y:set.y iIn Repl x minus_SNo -> SNo y hyp finite (Repl x minus_SNo) claim Repl x minus_SNo != Empty -> ?y:set.SNo_min_of x y