let X, Y be non empty MetrSpace; for x, y, z being Element of [:the carrier of X,the carrier of Y:] holds (dist_cart2 X,Y) . x,z <= ((dist_cart2 X,Y) . x,y) + ((dist_cart2 X,Y) . y,z)
let x, y, z be Element of [:the carrier of X,the carrier of Y:]; (dist_cart2 X,Y) . x,z <= ((dist_cart2 X,Y) . x,y) + ((dist_cart2 X,Y) . y,z)
reconsider x1 = x `1 , y1 = y `1 , z1 = z `1 as Element of X by MCART_1:10;
reconsider x2 = x `2 , y2 = y `2 , z2 = z `2 as Element of Y by MCART_1:10;
A1:
y = [y1,y2]
by MCART_1:24;
set d6 = dist y2,z2;
set d5 = dist x2,y2;
set d4 = dist x2,z2;
set d3 = dist y1,z1;
set d2 = dist x1,y1;
set d1 = dist x1,z1;
A2:
z = [z1,z2]
by MCART_1:24;
A3:
x = [x1,x2]
by MCART_1:24;
then A4:
(dist_cart2 X,Y) . x,z = (dist x1,z1) + (dist x2,z2)
by A2, Def1;
A5:
( dist x1,z1 <= (dist x1,y1) + (dist y1,z1) & dist x2,z2 <= (dist x2,y2) + (dist y2,z2) )
by METRIC_1:4;
((dist x1,y1) + (dist y1,z1)) + ((dist x2,y2) + (dist y2,z2)) =
((dist x1,y1) + (dist x2,y2)) + ((dist y1,z1) + (dist y2,z2))
.=
((dist_cart2 X,Y) . x,y) + ((dist y1,z1) + (dist y2,z2))
by A3, A1, Def1
.=
((dist_cart2 X,Y) . x,y) + ((dist_cart2 X,Y) . y,z)
by A1, A2, Def1
;
hence
(dist_cart2 X,Y) . x,z <= ((dist_cart2 X,Y) . x,y) + ((dist_cart2 X,Y) . y,z)
by A5, A4, XREAL_1:9; verum