let R be Relation; :: thesis: ( R is empty implies R is negative-yielding )
assume R is empty ; :: thesis: R is negative-yielding
then for x being Real st x in rng R holds
x < 0 ;
hence R is negative-yielding by PARTFUN3:def 2; :: thesis: verum