:: deftheorem defFy defines Field-yielding FIELD_12:def 3 :
for f being Relation holds
( f is Field-yielding iff for x being object st x in rng f holds
x is Field );