:: deftheorem Def1 defines positive-yielding PARTFUN3:def 1 :
for R being Relation holds
( R is positive-yielding iff for r being Real st r in rng R holds
0 < r );