:: deftheorem defines nonnegative SUPINF_2:def 11 :
for R being Relation holds
( R is nonnegative iff rng R is nonnegative );