:: deftheorem defines are_in_tolerance_wrt TAXONOM1:def 6 :
for M being MetrStruct
for a being Real
for x, y being Element of M holds
( x,y are_in_tolerance_wrt a iff dist (x,y) <= a );