:: deftheorem Def7 defines dist_toler TAXONOM1:def 7 :
for M being non empty MetrStruct
for a being Real
for b₃ being Relation of M holds
( b₃ = dist_toler (M,a) iff for x, y being Element of M holds
( [x,y] in b₃ iff x,y are_in_tolerance_wrt a ) );