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_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 , z1 = z `1_3 , z2 = z `2_3 , z3 = z `3_3 as Element of REAL ;

A1: x = [x1,x2,x3] ;

set d9 = real_dist . (y3,z3);

set d5 = real_dist . (x2,y2);

set d6 = real_dist . (y2,z2);

set d1 = real_dist . (x1,z1);

set d2 = real_dist . (x1,y1);

A2: y = [y1,y2,y3] ;

real_dist . (y3,z3) = |.(y3 - z3).| by METRIC_1:def 12;

then A3: 0 <= real_dist . (y3,z3) by COMPLEX1:46;

real_dist . (y2,z2) = |.(y2 - z2).| by METRIC_1:def 12;

then A4: 0 <= real_dist . (y2,z2) by COMPLEX1:46;

real_dist . (x2,y2) = |.(x2 - y2).| by METRIC_1:def 12;

then A5: 0 <= real_dist . (x2,y2) by COMPLEX1:46;

set d7 = real_dist . (x3,z3);

set d8 = real_dist . (x3,y3);

set d3 = real_dist . (y1,z1);

set d4 = real_dist . (x2,z2);

A6: z = [z1,z2,z3] ;

real_dist . (x3,z3) = |.(x3 - z3).| by METRIC_1:def 12;

then 0 <= real_dist . (x3,z3) by COMPLEX1:46;

then A7: (real_dist . (x3,z3)) ^2 <= ((real_dist . (x3,y3)) + (real_dist . (y3,z3))) ^2 by METRIC_1:10, SQUARE_1:15;

real_dist . (x2,z2) = |.(x2 - z2).| by METRIC_1:def 12;

then 0 <= real_dist . (x2,z2) by COMPLEX1:46;

then A8: (real_dist . (x2,z2)) ^2 <= ((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2 by METRIC_1:10, SQUARE_1:15;

real_dist . (x1,z1) = |.(x1 - z1).| by METRIC_1:def 12;

then 0 <= real_dist . (x1,z1) by COMPLEX1:46;

then (real_dist . (x1,z1)) ^2 <= ((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2 by METRIC_1:10, SQUARE_1:15;

then ((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 A8, XREAL_1:7;

then A9: (((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 A7, XREAL_1:7;

( 0 <= (real_dist . (x1,z1)) ^2 & 0 <= (real_dist . (x2,z2)) ^2 ) by XREAL_1:63;

then A10: 0 + 0 <= ((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2) by XREAL_1:7;

0 <= (real_dist . (x3,z3)) ^2 by XREAL_1:63;

then 0 + 0 <= (((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2)) + ((real_dist . (x3,z3)) ^2) by A10, XREAL_1:7;

then A11: 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 A9, SQUARE_1:26;

real_dist . (x3,y3) = |.(x3 - y3).| by METRIC_1:def 12;

then A12: 0 <= real_dist . (x3,y3) by COMPLEX1:46;

real_dist . (y1,z1) = |.(y1 - z1).| by METRIC_1:def 12;

then A13: 0 <= real_dist . (y1,z1) by COMPLEX1:46;

real_dist . (x1,y1) = |.(x1 - y1).| by METRIC_1:def 12;

then 0 <= real_dist . (x1,y1) by COMPLEX1:46;

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 A13, A5, A4, A12, A3, Lm2;

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 A11, 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, A6, Def22;

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, A2, Def22;

hence Eukl_dist3 . (x,z) <= (Eukl_dist3 . (x,y)) + (Eukl_dist3 . (y,z)) by A2, A6, Def22; :: thesis: verum

reconsider x1 = x `1_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 , z1 = z `1_3 , z2 = z `2_3 , z3 = z `3_3 as Element of REAL ;

A1: x = [x1,x2,x3] ;

set d9 = real_dist . (y3,z3);

set d5 = real_dist . (x2,y2);

set d6 = real_dist . (y2,z2);

set d1 = real_dist . (x1,z1);

set d2 = real_dist . (x1,y1);

A2: y = [y1,y2,y3] ;

real_dist . (y3,z3) = |.(y3 - z3).| by METRIC_1:def 12;

then A3: 0 <= real_dist . (y3,z3) by COMPLEX1:46;

real_dist . (y2,z2) = |.(y2 - z2).| by METRIC_1:def 12;

then A4: 0 <= real_dist . (y2,z2) by COMPLEX1:46;

real_dist . (x2,y2) = |.(x2 - y2).| by METRIC_1:def 12;

then A5: 0 <= real_dist . (x2,y2) by COMPLEX1:46;

set d7 = real_dist . (x3,z3);

set d8 = real_dist . (x3,y3);

set d3 = real_dist . (y1,z1);

set d4 = real_dist . (x2,z2);

A6: z = [z1,z2,z3] ;

real_dist . (x3,z3) = |.(x3 - z3).| by METRIC_1:def 12;

then 0 <= real_dist . (x3,z3) by COMPLEX1:46;

then A7: (real_dist . (x3,z3)) ^2 <= ((real_dist . (x3,y3)) + (real_dist . (y3,z3))) ^2 by METRIC_1:10, SQUARE_1:15;

real_dist . (x2,z2) = |.(x2 - z2).| by METRIC_1:def 12;

then 0 <= real_dist . (x2,z2) by COMPLEX1:46;

then A8: (real_dist . (x2,z2)) ^2 <= ((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2 by METRIC_1:10, SQUARE_1:15;

real_dist . (x1,z1) = |.(x1 - z1).| by METRIC_1:def 12;

then 0 <= real_dist . (x1,z1) by COMPLEX1:46;

then (real_dist . (x1,z1)) ^2 <= ((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2 by METRIC_1:10, SQUARE_1:15;

then ((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 A8, XREAL_1:7;

then A9: (((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 A7, XREAL_1:7;

( 0 <= (real_dist . (x1,z1)) ^2 & 0 <= (real_dist . (x2,z2)) ^2 ) by XREAL_1:63;

then A10: 0 + 0 <= ((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2) by XREAL_1:7;

0 <= (real_dist . (x3,z3)) ^2 by XREAL_1:63;

then 0 + 0 <= (((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2)) + ((real_dist . (x3,z3)) ^2) by A10, XREAL_1:7;

then A11: 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 A9, SQUARE_1:26;

real_dist . (x3,y3) = |.(x3 - y3).| by METRIC_1:def 12;

then A12: 0 <= real_dist . (x3,y3) by COMPLEX1:46;

real_dist . (y1,z1) = |.(y1 - z1).| by METRIC_1:def 12;

then A13: 0 <= real_dist . (y1,z1) by COMPLEX1:46;

real_dist . (x1,y1) = |.(x1 - y1).| by METRIC_1:def 12;

then 0 <= real_dist . (x1,y1) by COMPLEX1:46;

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 A13, A5, A4, A12, A3, Lm2;

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 A11, 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, A6, Def22;

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, A2, Def22;

hence Eukl_dist3 . (x,z) <= (Eukl_dist3 . (x,y)) + (Eukl_dist3 . (y,z)) by A2, A6, Def22; :: thesis: verum