const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const omega : set const finite : set prop const SNoL : set set axiom SNoS_omega_SNoL_finite: !x:set.x iIn SNoS_ omega -> finite (SNoL x) const SNo : set prop const Empty : set const SNo_max_of : set set prop 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 x iIn SNoS_ omega hyp SNoL x != Empty claim (!y:set.y iIn SNoL x -> SNo y) -> ?y:set.SNo_max_of (SNoL x) y