let X, Y, Z be non empty MetrSpace; for x, y, z being Element of [: the carrier of X, the carrier of Y, the carrier of Z:] holds (dist_cart3S (X,Y,Z)) . (x,z) <= ((dist_cart3S (X,Y,Z)) . (x,y)) + ((dist_cart3S (X,Y,Z)) . (y,z))
let x, y, z be Element of [: the carrier of X, the carrier of Y, the carrier of Z:]; (dist_cart3S (X,Y,Z)) . (x,z) <= ((dist_cart3S (X,Y,Z)) . (x,y)) + ((dist_cart3S (X,Y,Z)) . (y,z))
reconsider x1 = x `1_3 , y1 = y `1_3 , z1 = z `1_3 as Element of X ;
reconsider x2 = x `2_3 , y2 = y `2_3 , z2 = z `2_3 as Element of Y ;
reconsider x3 = x `3_3 , y3 = y `3_3 , z3 = z `3_3 as Element of Z ;
A1:
x = [x1,x2,x3]
;
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]
;
( dist (x3,z3) <= (dist (x3,y3)) + (dist (y3,z3)) & 0 <= dist (x3,z3) )
by METRIC_1:4, METRIC_1:5;
then A3:
(dist (x3,z3)) ^2 <= ((dist (x3,y3)) + (dist (y3,z3))) ^2
by SQUARE_1:15;
A4:
( 0 <= dist (x3,y3) & 0 <= dist (y3,z3) )
by METRIC_1:5;
set d4 = dist (x2,z2);
set d5 = dist (x2,y2);
set d6 = dist (y2,z2);
A5:
z = [z1,z2,z3]
;
( dist (x2,z2) <= (dist (x2,y2)) + (dist (y2,z2)) & 0 <= dist (x2,z2) )
by METRIC_1:4, METRIC_1:5;
then A6:
(dist (x2,z2)) ^2 <= ((dist (x2,y2)) + (dist (y2,z2))) ^2
by SQUARE_1:15;
A7:
( 0 <= dist (x2,y2) & 0 <= dist (y2,z2) )
by METRIC_1:5;
( 0 <= (dist (x1,z1)) ^2 & 0 <= (dist (x2,z2)) ^2 )
by XREAL_1:63;
then A8:
0 + 0 <= ((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)
by XREAL_1:7;
( dist (x1,z1) <= (dist (x1,y1)) + (dist (y1,z1)) & 0 <= dist (x1,z1) )
by METRIC_1:4, METRIC_1:5;
then
(dist (x1,z1)) ^2 <= ((dist (x1,y1)) + (dist (y1,z1))) ^2
by SQUARE_1:15;
then
((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2) <= (((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2)
by A6, XREAL_1:7;
then A9:
(((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)) + ((dist (x3,z3)) ^2) <= ((((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2)) + (((dist (x3,y3)) + (dist (y3,z3))) ^2)
by A3, XREAL_1:7;
0 <= (dist (x3,z3)) ^2
by XREAL_1:63;
then
0 + 0 <= (((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)) + ((dist (x3,z3)) ^2)
by A8, XREAL_1:7;
then A10:
sqrt ((((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)) + ((dist (x3,z3)) ^2)) <= sqrt (((((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2)) + (((dist (x3,y3)) + (dist (y3,z3))) ^2))
by A9, SQUARE_1:26;
( 0 <= dist (x1,y1) & 0 <= dist (y1,z1) )
by METRIC_1:5;
then
sqrt (((((dist (x1,y1)) + (dist (y1,z1))) ^2) + (((dist (x2,y2)) + (dist (y2,z2))) ^2)) + (((dist (x3,y3)) + (dist (y3,z3))) ^2)) <= (sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))) + (sqrt ((((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2)) + ((dist (y3,z3)) ^2)))
by A7, A4, Lm2;
then
sqrt ((((dist (x1,z1)) ^2) + ((dist (x2,z2)) ^2)) + ((dist (x3,z3)) ^2)) <= (sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))) + (sqrt ((((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2)) + ((dist (y3,z3)) ^2)))
by A10, XXREAL_0:2;
then
(dist_cart3S (X,Y,Z)) . (x,z) <= (sqrt ((((dist (x1,y1)) ^2) + ((dist (x2,y2)) ^2)) + ((dist (x3,y3)) ^2))) + (sqrt ((((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2)) + ((dist (y3,z3)) ^2)))
by A1, A5, Def13;
then
(dist_cart3S (X,Y,Z)) . (x,z) <= ((dist_cart3S (X,Y,Z)) . (x,y)) + (sqrt ((((dist (y1,z1)) ^2) + ((dist (y2,z2)) ^2)) + ((dist (y3,z3)) ^2)))
by A1, A2, Def13;
hence
(dist_cart3S (X,Y,Z)) . (x,z) <= ((dist_cart3S (X,Y,Z)) . (x,y)) + ((dist_cart3S (X,Y,Z)) . (y,z))
by A2, A5, Def13; verum