take f = {} ; :: thesis: f is infinite-yielding
let I be set ; :: according to MSAFREE5:def 8 :: thesis: ( I in rng f implies I is infinite )
assume I in rng f ; :: thesis: I is infinite
hence I is infinite ; :: thesis: verum