theorem Th22: :: TAXONOM1:22

for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being Real st low_toler (f,a) is_reflexive_in X & f is symmetric holds
(low_toler (f,a)) [*] is Equivalence_Relation of X