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