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 :: thesis: for x, y being Element of M holds the distance of M . (x,y) >= 0
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 ;
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 6, METRIC_1:def 7;
hence Class R = SmallestPartition the carrier of M by A1, Th24; :: thesis: verum