let x, y, z be Element of [:REAL,REAL:]; :: thesis: Eukl_dist2 . (x,z) <= (Eukl_dist2 . (x,y)) + (Eukl_dist2 . (y,z))
reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 , z1 = z `1 , z2 = z `2 as Element of REAL ;
A1: x = [x1,x2] ;
set d5 = real_dist . (x2,y2);
set d3 = real_dist . (y1,z1);
set d1 = real_dist . (x1,z1);
A2: y = [y1,y2] ;
set d6 = real_dist . (y2,z2);
set d4 = real_dist . (x2,z2);
set d2 = real_dist . (x1,y1);
A3: z = [z1,z2] ;
real_dist . (x2,z2) = |.(x2 - z2).| by METRIC_1:def 12;
then 0 <= real_dist . (x2,z2) by COMPLEX1:46;
then A4: (real_dist . (x2,z2)) ^2 <= ((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2 by METRIC_1:10, SQUARE_1:15;
( 0 <= (real_dist . (x1,z1)) ^2 & 0 <= (real_dist . (x2,z2)) ^2 ) by XREAL_1:63;
then A5: 0 + 0 <= ((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2) by XREAL_1:7;
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 A4, XREAL_1:7;
then A6: sqrt (((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2)) <= sqrt ((((real_dist . (x1,y1)) + (real_dist . (y1,z1))) ^2) + (((real_dist . (x2,y2)) + (real_dist . (y2,z2))) ^2)) by A5, SQUARE_1:26;
real_dist . (y2,z2) = |.(y2 - z2).| by METRIC_1:def 12;
then A7: 0 <= real_dist . (y2,z2) by COMPLEX1:46;
real_dist . (x2,y2) = |.(x2 - y2).| by METRIC_1:def 12;
then A8: 0 <= real_dist . (x2,y2) by COMPLEX1:46;
real_dist . (y1,z1) = |.(y1 - z1).| by METRIC_1:def 12;
then A9: 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)) <= (sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))) + (sqrt (((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2))) by A9, A8, A7, Th12;
then sqrt (((real_dist . (x1,z1)) ^2) + ((real_dist . (x2,z2)) ^2)) <= (sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))) + (sqrt (((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2))) by A6, XXREAL_0:2;
then Eukl_dist2 . (x,z) <= (sqrt (((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2))) + (sqrt (((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2))) by A1, A3, Def18;
then Eukl_dist2 . (x,z) <= (Eukl_dist2 . (x,y)) + (sqrt (((real_dist . (y1,z1)) ^2) + ((real_dist . (y2,z2)) ^2))) by A1, A2, Def18;
hence Eukl_dist2 . (x,z) <= (Eukl_dist2 . (x,y)) + (Eukl_dist2 . (y,z)) by A2, A3, Def18; :: thesis: verum