let x, y, z be Element of [:REAL ,REAL ,REAL :]; taxi_dist3 . x,z <= (taxi_dist3 . x,y) + (taxi_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]
by MCART_1:48;
set d7 = real_dist . x3,z3;
set d8 = real_dist . x3,y3;
set d3 = real_dist . y1,z1;
set d4 = real_dist . x2,z2;
A2:
z = [z1,z2,z3]
by MCART_1:48;
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;
A3:
y = [y1,y2,y3]
by MCART_1:48;
set d10 = (real_dist . x1,z1) + (real_dist . x2,z2);
( real_dist . x1,z1 <= (real_dist . x1,y1) + (real_dist . y1,z1) & real_dist . x2,z2 <= (real_dist . x2,y2) + (real_dist . y2,z2) )
by METRIC_1:11;
then A4:
(real_dist . x1,z1) + (real_dist . x2,z2) <= ((real_dist . x1,y1) + (real_dist . y1,z1)) + ((real_dist . x2,y2) + (real_dist . y2,z2))
by XREAL_1:9;
real_dist . x3,z3 <= (real_dist . x3,y3) + (real_dist . y3,z3)
by METRIC_1:11;
then A5:
((real_dist . x1,z1) + (real_dist . x2,z2)) + (real_dist . x3,z3) <= (((real_dist . x1,y1) + (real_dist . y1,z1)) + ((real_dist . x2,y2) + (real_dist . y2,z2))) + ((real_dist . x3,y3) + (real_dist . y3,z3))
by A4, XREAL_1:9;
(((real_dist . x1,y1) + (real_dist . y1,z1)) + ((real_dist . x2,y2) + (real_dist . y2,z2))) + ((real_dist . x3,y3) + (real_dist . y3,z3)) =
(((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3)) + (((real_dist . y1,z1) + (real_dist . y2,z2)) + (real_dist . y3,z3))
.=
(taxi_dist3 . x,y) + (((real_dist . y1,z1) + (real_dist . y2,z2)) + (real_dist . y3,z3))
by A1, A3, Def11
.=
(taxi_dist3 . x,y) + (taxi_dist3 . y,z)
by A3, A2, Def11
;
hence
taxi_dist3 . x,z <= (taxi_dist3 . x,y) + (taxi_dist3 . y,z)
by A1, A2, A5, Def11; verum