:: deftheorem Def2 defines negative-yielding PARTFUN3:def 2 :
for R being Relation holds
( R is negative-yielding iff for r being Real st r in rng R holds
0 > r );