let x, y, z be Element of [:REAL ,REAL ,REAL :]; :: thesis: Eukl_dist3 . x,z <= (Eukl_dist3 . x,y) + (Eukl_dist3 . y,z)
reconsider x1 = x `1 , x2 = x `2 , x3 = x `3 , y1 = y `1 , y2 = y `2 , y3 = y `3 , z1 = z `1 , z2 = z `2 , z3 = z `3 as Element of REAL ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] & z = [z1,z2,z3] ) by MCART_1:48;
set d1 = real_dist . x1,z1;
set d2 = real_dist . x1,y1;
set d3 = real_dist . y1,z1;
set d4 = real_dist . x2,z2;
set d5 = real_dist . x2,y2;
set d6 = real_dist . y2,z2;
set d7 = real_dist . x3,z3;
set d8 = real_dist . x3,y3;
set d9 = real_dist . y3,z3;
real_dist . x1,z1 = abs (x1 - z1) by METRIC_1:def 13;
then 0 <= real_dist . x1,z1 by COMPLEX1:132;
then A2: (real_dist . x1,z1) ^2 <= ((real_dist . x1,y1) + (real_dist . y1,z1)) ^2 by METRIC_1:11, SQUARE_1:77;
real_dist . x2,z2 = abs (x2 - z2) by METRIC_1:def 13;
then 0 <= real_dist . x2,z2 by COMPLEX1:132;
then A3: (real_dist . x2,z2) ^2 <= ((real_dist . x2,y2) + (real_dist . y2,z2)) ^2 by METRIC_1:11, SQUARE_1:77;
real_dist . x3,z3 = abs (x3 - z3) by METRIC_1:def 13;
then 0 <= real_dist . x3,z3 by COMPLEX1:132;
then A4: (real_dist . x3,z3) ^2 <= ((real_dist . x3,y3) + (real_dist . y3,z3)) ^2 by METRIC_1:11, SQUARE_1:77;
((real_dist . x1,z1) ^2 ) + ((real_dist . x2,z2) ^2 ) <= (((real_dist . x1,y1) + (real_dist . y1,z1)) ^2 ) + (((real_dist . x2,y2) + (real_dist . y2,z2)) ^2 ) by A2, A3, XREAL_1:9;
then A5: (((real_dist . x1,z1) ^2 ) + ((real_dist . x2,z2) ^2 )) + ((real_dist . x3,z3) ^2 ) <= ((((real_dist . x1,y1) + (real_dist . y1,z1)) ^2 ) + (((real_dist . x2,y2) + (real_dist . y2,z2)) ^2 )) + (((real_dist . x3,y3) + (real_dist . y3,z3)) ^2 ) by A4, XREAL_1:9;
A6: 0 <= (real_dist . x1,z1) ^2 by XREAL_1:65;
0 <= (real_dist . x2,z2) ^2 by XREAL_1:65;
then A7: 0 + 0 <= ((real_dist . x1,z1) ^2 ) + ((real_dist . x2,z2) ^2 ) by A6, XREAL_1:9;
0 <= (real_dist . x3,z3) ^2 by XREAL_1:65;
then 0 + 0 <= (((real_dist . x1,z1) ^2 ) + ((real_dist . x2,z2) ^2 )) + ((real_dist . x3,z3) ^2 ) by A7, XREAL_1:9;
then A8: sqrt ((((real_dist . x1,z1) ^2 ) + ((real_dist . x2,z2) ^2 )) + ((real_dist . x3,z3) ^2 )) <= sqrt (((((real_dist . x1,y1) + (real_dist . y1,z1)) ^2 ) + (((real_dist . x2,y2) + (real_dist . y2,z2)) ^2 )) + (((real_dist . x3,y3) + (real_dist . y3,z3)) ^2 )) by A5, SQUARE_1:94;
A9: real_dist . x1,y1 = abs (x1 - y1) by METRIC_1:def 13;
A10: real_dist . y1,z1 = abs (y1 - z1) by METRIC_1:def 13;
A11: real_dist . x2,y2 = abs (x2 - y2) by METRIC_1:def 13;
A12: real_dist . y2,z2 = abs (y2 - z2) by METRIC_1:def 13;
A13: real_dist . x3,y3 = abs (x3 - y3) by METRIC_1:def 13;
real_dist . y3,z3 = abs (y3 - z3) by METRIC_1:def 13;
then ( 0 <= real_dist . x1,y1 & 0 <= real_dist . y1,z1 & 0 <= real_dist . x2,y2 & 0 <= real_dist . y2,z2 & 0 <= real_dist . x3,y3 & 0 <= real_dist . y3,z3 ) by A9, A10, A11, A12, A13, COMPLEX1:132;
then sqrt (((((real_dist . x1,y1) + (real_dist . y1,z1)) ^2 ) + (((real_dist . x2,y2) + (real_dist . y2,z2)) ^2 )) + (((real_dist . x3,y3) + (real_dist . y3,z3)) ^2 )) <= (sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 ))) + (sqrt ((((real_dist . y1,z1) ^2 ) + ((real_dist . y2,z2) ^2 )) + ((real_dist . y3,z3) ^2 ))) by Lm1;
then sqrt ((((real_dist . x1,z1) ^2 ) + ((real_dist . x2,z2) ^2 )) + ((real_dist . x3,z3) ^2 )) <= (sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 ))) + (sqrt ((((real_dist . y1,z1) ^2 ) + ((real_dist . y2,z2) ^2 )) + ((real_dist . y3,z3) ^2 ))) by A8, XXREAL_0:2;
then Eukl_dist3 . x,z <= (sqrt ((((real_dist . x1,y1) ^2 ) + ((real_dist . x2,y2) ^2 )) + ((real_dist . x3,y3) ^2 ))) + (sqrt ((((real_dist . y1,z1) ^2 ) + ((real_dist . y2,z2) ^2 )) + ((real_dist . y3,z3) ^2 ))) by A1, Def13;
then Eukl_dist3 . x,z <= (Eukl_dist3 . x,y) + (sqrt ((((real_dist . y1,z1) ^2 ) + ((real_dist . y2,z2) ^2 )) + ((real_dist . y3,z3) ^2 ))) by A1, Def13;
hence Eukl_dist3 . x,z <= (Eukl_dist3 . x,y) + (Eukl_dist3 . y,z) by A1, Def13; :: thesis: verum