:: deftheorem defines nonnegative TAXONOM1:def 4 :
for X being set
for f being PartFunc of [:X,X:],REAL holds
( f is nonnegative iff for x, y being Element of X holds f . (x,y) >= 0 );