for M being MetrSpace
for x, y being Element of M st x <> y holds
0 < dist (x,y)