let M be non empty Reflexive discerning MetrStruct ; :: thesis: for x, y being Element of M holds
( x tolerates y iff x = y )
let x, y be Element of M; :: thesis: ( x tolerates y iff x = y )
( x tolerates y implies x = y )

proof

assume x tolerates y ; :: thesis: x = y
then dist x,y = 0 by Def1;
hence x = y by METRIC_1:2; :: thesis: verum

end;

hence ( x tolerates y iff x = y ) ; :: thesis: verum