let R be Relation; :: thesis: ( R is {{}} -valued iff R is empty-yielding )
( R is {{}} -valued iff rng R c= {{}} ) by RELAT_1:def 19;
hence ( R is {{}} -valued iff R is empty-yielding ) by RELAT_1:def 15; :: thesis: verum