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;
now :: thesis: not Y0 c= {{}}
assume Y0 c= {{}} ; :: thesis: contradiction
then ( the Element of Y0 in {{}} & the Element of Y0 in Y ) by TARSKI:def 3;
hence contradiction ; :: thesis: verum
end;
hence not R is empty-yielding ; :: thesis: verum