const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const omega : set const finite : set prop const SNoR : set set axiom SNoS_omega_SNoR_finite: !x:set.x iIn SNoS_ omega -> finite (SNoR x) const SNo : set prop const Empty : set const SNo_min_of : set set prop axiom finite_min_exists: !x:set.(!y:set.y iIn x -> SNo y) -> finite x -> x != Empty -> ?y:set.SNo_min_of x y var x:set hyp x iIn SNoS_ omega hyp SNoR x != Empty claim (!y:set.y iIn SNoR x -> SNo y) -> ?y:set.SNo_min_of (SNoR x) y