theorem Th7: :: METRIC_1:7

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