let R be Relation; :: thesis: ( R is positive-yielding implies ( R is nonnegative-yielding & R is non-empty ) )
assume A1: for r being real number st r in rng R holds
0 < r ; :: according to PARTFUN3:def 1 :: thesis: ( R is nonnegative-yielding & R is non-empty )
thus R is nonnegative-yielding :: thesis: R is non-empty

proof

let r be real number ; :: according to PARTFUN3:def 4 :: thesis: ( r in rng R implies 0 <= r )
thus ( r in rng R implies 0 <= r ) by A1; :: thesis: verum

end;

assume not R is non-empty ; :: thesis: contradiction
then 0 in rng R by RELAT_1:def 9;
hence contradiction by A1; :: thesis: verum