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