:: deftheorem defines tolerates METRIC_2:def 1 :
for M being non empty MetrStruct
for x, y being Element of M holds
( x tolerates y iff dist (x,y) = 0 );