theorem Th1: :: METRIC_3:1

for X, Y being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y:] holds
( (dist_cart2 (X,Y)) . (x,y) = 0 iff x = y )