:: deftheorem Def3 defines nonpositive-yielding PARTFUN3:def 3 :
for R being Relation holds
( R is nonpositive-yielding iff for r being Real st r in rng R holds
0 >= r );