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

now

let x, y be Element of M; :: thesis: the distance of M . x,y >= 0
dist x,y >= 0 by METRIC_1:5;
hence the distance of M . x,y >= 0 by METRIC_1:def 1; :: thesis: verum

end;

then A1: the distance of M is nonnegative by Def4;
let R be Equivalence_Relation of M; :: thesis: ( R = (dist_toler M,0 ) [*] implies Class R = SmallestPartition the carrier of M )
assume R = (dist_toler M,0 ) [*] ; :: thesis: Class R = SmallestPartition the carrier of M
then ( the distance of M is Reflexive & the distance of M is discerning & (low_toler the distance of M,0 ) [*] = R ) by Th33, METRIC_1:def 7, METRIC_1:def 8;
hence Class R = SmallestPartition the carrier of M by A1, Th24; :: thesis: verum