theorem Th21: :: TAXONOM1:21

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