theorem Th27: :: TAXONOM1:27

for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being Real st z = rng f & A >= max z holds
for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}