:: deftheorem INF defines infinite-yielding MSAFREE5:def 8 :
for R being Relation holds
( R is infinite-yielding iff for I being set st I in rng R holds
I is infinite );