let x be Element of M; :: thesis: x tolerates x
dist (x,x) = 0 by METRIC_1:1;
hence x tolerates x by Def1; :: thesis: verum