let R be Relation; :: thesis: ( R is negative-yielding implies ( R is nonpositive-yielding & R is non-empty ) )
assume A2: for r being real number st r in rng R holds
0 > r ; :: according to PARTFUN3:def 2 :: thesis: ( R is nonpositive-yielding & R is non-empty )
thus R is nonpositive-yielding :: thesis: R is non-empty

proof

let r be real number ; :: according to PARTFUN3:def 3 :: thesis: ( r in rng R implies 0 >= r )
thus ( r in rng R implies 0 >= r ) by A2; :: thesis: verum

end;

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