theorem Th40: :: TAXONOM1:40

for M being non empty Reflexive symmetric bounded MetrStruct
for R being Equivalence_Relation of M
for a being non negative Real st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds
Class R = { the carrier of M}