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