theorem ME7: :: ROUGHIF2:43

for X being non empty set
for f being nonnegative-yielding Reflexive discerning triangle Function of [:X,X:],REAL
for x, y being Element of X st x <> y holds
f . (x,y) > 0