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 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

Class R = SmallestPartition the carrier of M

now :: thesis: for x, y being Element of M holds the distance of M . (x,y) >= 0

then A1:
the distance of M is nonnegative
;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;dist (x,y) >= 0 by METRIC_1:5;

hence the distance of M . (x,y) >= 0 by METRIC_1:def 1; :: thesis: verum

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