:: deftheorem Def2 defines finite-yielding FINSET_1:def 2 :
for R being Relation holds
( R is finite-yielding iff for x being set st x in rng R holds
x is finite );