let X, Y be non empty MetrSpace; :: thesis: for x, y, z being Element of [:the carrier of X,the carrier of Y:] holds (dist_cart2S X,Y) . x,z <= ((dist_cart2S X,Y) . x,y) + ((dist_cart2S X,Y) . y,z)
let x, y, z be Element of [:the carrier of X,the carrier of Y:]; :: thesis: (dist_cart2S X,Y) . x,z <= ((dist_cart2S X,Y) . x,y) + ((dist_cart2S 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: ( x = [x1,x2] & y = [y1,y2] & z = [z1,z2] ) by MCART_1:24;
set d1 = dist x1,z1;
set d2 = dist x1,y1;
set d3 = dist y1,z1;
set d4 = dist x2,z2;
set d5 = dist x2,y2;
set d6 = dist y2,z2;
A2: dist x1,z1 <= (dist x1,y1) + (dist y1,z1) by METRIC_1:4;
0 <= dist x1,z1 by METRIC_1:5;
then A3: (dist x1,z1) ^2 <= ((dist x1,y1) + (dist y1,z1)) ^2 by A2, SQUARE_1:77;
A4: dist x2,z2 <= (dist x2,y2) + (dist y2,z2) by METRIC_1:4;
0 <= dist x2,z2 by METRIC_1:5;
then (dist x2,z2) ^2 <= ((dist x2,y2) + (dist y2,z2)) ^2 by A4, SQUARE_1:77;
then A5: ((dist x1,z1) ^2 ) + ((dist x2,z2) ^2 ) <= (((dist x1,y1) + (dist y1,z1)) ^2 ) + (((dist x2,y2) + (dist y2,z2)) ^2 ) by A3, XREAL_1:9;
A6: 0 <= (dist x1,z1) ^2 by XREAL_1:65;
0 <= (dist x2,z2) ^2 by XREAL_1:65;
then 0 + 0 <= ((dist x1,z1) ^2 ) + ((dist x2,z2) ^2 ) by A6, XREAL_1:9;
then A7: sqrt (((dist x1,z1) ^2 ) + ((dist x2,z2) ^2 )) <= sqrt ((((dist x1,y1) + (dist y1,z1)) ^2 ) + (((dist x2,y2) + (dist y2,z2)) ^2 )) by A5, SQUARE_1:94;
( 0 <= dist x1,y1 & 0 <= dist y1,z1 & 0 <= dist x2,y2 & 0 <= dist y2,z2 ) by METRIC_1:5;
then sqrt ((((dist x1,y1) + (dist y1,z1)) ^2 ) + (((dist x2,y2) + (dist y2,z2)) ^2 )) <= (sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 ))) + (sqrt (((dist y1,z1) ^2 ) + ((dist y2,z2) ^2 ))) by Th5;
then sqrt (((dist x1,z1) ^2 ) + ((dist x2,z2) ^2 )) <= (sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 ))) + (sqrt (((dist y1,z1) ^2 ) + ((dist y2,z2) ^2 ))) by A7, XXREAL_0:2;
then (dist_cart2S X,Y) . x,z <= (sqrt (((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 ))) + (sqrt (((dist y1,z1) ^2 ) + ((dist y2,z2) ^2 ))) by A1, Def1;
then (dist_cart2S X,Y) . x,z <= ((dist_cart2S X,Y) . x,y) + (sqrt (((dist y1,z1) ^2 ) + ((dist y2,z2) ^2 ))) by A1, Def1;
hence (dist_cart2S X,Y) . x,z <= ((dist_cart2S X,Y) . x,y) + ((dist_cart2S X,Y) . y,z) by A1, Def1; :: thesis: verum