:: deftheorem Def3 defines RelStr-yielding YELLOW_1:def 3 :
for R being Relation holds
( R is RelStr-yielding iff for v being set st v in rng R holds
v is RelStr );