:: deftheorem Def8 defines reflexive-yielding WAYBEL_3:def 8 :
for f being Relation holds
( f is reflexive-yielding iff for S being RelStr st S in rng f holds
S is reflexive );