:: deftheorem Non defines nonnegative-yielding ROUGHIF2:def 9 :
for X being non empty set
for f being Function of [:X,X:],REAL holds
( f is nonnegative-yielding iff for x, y being Element of X holds f . (x,y) >= 0 );