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_4 , y1 = y `1_4 , z1 = z `1_4 as Element of X ;
reconsider x2 = x `2_4 , y2 = y `2_4 , z2 = z `2_4 as Element of Y ;
reconsider x3 = x `3_4 , y3 = y `3_4 , z3 = z `3_4 as Element of Z ;
reconsider x4 = x `4_4 , y4 = y `4_4 , z4 = z `4_4 as Element of W ;
A1:
x = [x1,x2,x3,x4]
;
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]
;
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]
;
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:7;
( 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:7;
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:7;
(((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