:: deftheorem Def4 defines nonnegative-yielding PARTFUN3:def 4 :
for R being Relation holds
( R is nonnegative-yielding iff for r being Real st r in rng R holds
0 <= r );