theorem Th11: :: METRIC_2:11

for M being non empty Reflexive discerning MetrStruct
for x, y being Element of M holds
( x tolerates y iff x = y ) by METRIC_1:2;