let X, Y, Z, W be 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)
let x, y, z be Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:]; (dist_cart4 X,Y,Z,W) . x,z <= ((dist_cart4 X,Y,Z,W) . x,y) + ((dist_cart4 X,Y,Z,W) . y,z)
reconsider x1 = x `1 , y1 = y `1 , z1 = z `1 as Element of X ;
reconsider x2 = x `2 , y2 = y `2 , z2 = z `2 as Element of Y ;
reconsider x3 = x `3 , y3 = y `3 , z3 = z `3 as Element of Z ;
reconsider x4 = x `4 , y4 = y `4 , z4 = z `4 as Element of W ;
A1:
x = [x1,x2,x3,x4]
by MCART_1:60;
set d7 = dist x3,z3;
set d8 = dist x3,y3;
set d9 = dist y3,z3;
set d1 = dist x1,z1;
set d2 = dist x1,y1;
set d3 = dist y1,z1;
A2:
y = [y1,y2,y3,y4]
by MCART_1:60;
set d10 = dist x4,z4;
set d11 = dist x4,y4;
set d12 = dist y4,z4;
set d4 = dist x2,z2;
set d5 = dist x2,y2;
set d6 = dist y2,z2;
A3:
z = [z1,z2,z3,z4]
by MCART_1:60;
set d16 = (dist x3,z3) + (dist x4,z4);
set d14 = (dist x1,z1) + (dist x2,z2);
set d17 = ((dist x3,y3) + (dist y3,z3)) + ((dist x4,y4) + (dist y4,z4));
set d15 = ((dist x1,y1) + (dist y1,z1)) + ((dist x2,y2) + (dist y2,z2));
( dist x3,z3 <= (dist x3,y3) + (dist y3,z3) & dist x4,z4 <= (dist x4,y4) + (dist y4,z4) )
by METRIC_1:4;
then A4:
(dist x3,z3) + (dist x4,z4) <= ((dist x3,y3) + (dist y3,z3)) + ((dist x4,y4) + (dist y4,z4))
by XREAL_1:9;
( dist x1,z1 <= (dist x1,y1) + (dist y1,z1) & dist x2,z2 <= (dist x2,y2) + (dist y2,z2) )
by METRIC_1:4;
then
(dist x1,z1) + (dist x2,z2) <= ((dist x1,y1) + (dist y1,z1)) + ((dist x2,y2) + (dist y2,z2))
by XREAL_1:9;
then A5:
((dist x1,z1) + (dist x2,z2)) + ((dist x3,z3) + (dist x4,z4)) <= (((dist x1,y1) + (dist y1,z1)) + ((dist x2,y2) + (dist y2,z2))) + (((dist x3,y3) + (dist y3,z3)) + ((dist x4,y4) + (dist y4,z4)))
by A4, XREAL_1:9;
(((dist x1,y1) + (dist y1,z1)) + ((dist x2,y2) + (dist y2,z2))) + (((dist x3,y3) + (dist y3,z3)) + ((dist x4,y4) + (dist y4,z4))) =
(((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4))) + (((dist y1,z1) + (dist y2,z2)) + ((dist y3,z3) + (dist y4,z4)))
.=
((dist_cart4 X,Y,Z,W) . x,y) + (((dist y1,z1) + (dist y2,z2)) + ((dist y3,z3) + (dist y4,z4)))
by A1, A2, Def7
.=
((dist_cart4 X,Y,Z,W) . x,y) + ((dist_cart4 X,Y,Z,W) . y,z)
by A2, A3, Def7
;
hence
(dist_cart4 X,Y,Z,W) . x,z <= ((dist_cart4 X,Y,Z,W) . x,y) + ((dist_cart4 X,Y,Z,W) . y,z)
by A1, A3, A5, Def7; verum