theorem Th36: :: TAXONOM1:36

for M being non empty MetrSpace
for R being Equivalence_Relation of M st R = (dist_toler (M,0)) [*] holds
Class R = SmallestPartition the carrier of M