let R be Relation; :: thesis: ( R is natural-valued implies R is nonnegative-yielding )
assume R is natural-valued ; :: thesis: R is nonnegative-yielding
then for r being Real st r in rng R holds
r >= 0 ;
hence R is nonnegative-yielding by PARTFUN3:def 4; :: thesis: verum