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