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 , 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 ;
A1:
x = [x1,x2,x3]
by MCART_1:48;
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]
by MCART_1:48;
( 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:77;
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]
by MCART_1:48;
( 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:77;
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:65;
then A8:
0 + 0 <= ((dist x1,z1) ^2 ) + ((dist x2,z2) ^2 )
by XREAL_1:9;
( 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:77;
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:9;
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:9;
0 <= (dist x3,z3) ^2
by XREAL_1:65;
then
0 + 0 <= (((dist x1,z1) ^2 ) + ((dist x2,z2) ^2 )) + ((dist x3,z3) ^2 )
by A8, XREAL_1:9;
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:94;
( 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, Lm1;
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, Def4;
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, Def4;
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, Def4; verum