theorem :: TAXONOM1:34

for M being non empty Reflexive symmetric MetrStruct
for a being Real
for T being Relation of the carrier of M, the carrier of M st T = dist_toler (M,a) & a >= 0 holds
T is Tolerance of the carrier of M