theorem Th13: :: METRIC_3:13

for X, Y being non empty MetrSpace
for x, y, z being Element of [: the carrier of X, the carrier of Y:] holds (dist_cart2S (X,Y)) . (x,z) <= ((dist_cart2S (X,Y)) . (x,y)) + ((dist_cart2S (X,Y)) . (y,z))