let R be Y -valued Relation; :: thesis: ( not R is empty implies not R is empty-yielding )
assume not R is empty ; :: thesis: not R is empty-yielding
then reconsider Y0 = rng R as non empty set ;
set y = the Element of Y0;
B0: Y0 c= Y by RELAT_1:def 19;

now

assume Y0 c= {{}} ; :: thesis: contradiction
then ( the Element of Y0 in {{}} & the Element of Y0 in Y ) by B0, TARSKI:def 3;
hence contradiction ; :: thesis: verum

end;

hence not R is empty-yielding by RELAT_1:def 15; :: thesis: verum