theorem Th20: :: TAXONOM1:20

for X being non empty set
for f being PartFunc of [:X,X:],REAL
for x, y being object st f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) holds
x = y