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