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_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 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]
;
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]
;
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:10;
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:7;
real_dist . (x3,z3) <= (real_dist . (x3,y3)) + (real_dist . (y3,z3))
by METRIC_1:10;
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:7;
(((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, Def20
.=
(taxi_dist3 . (x,y)) + (taxi_dist3 . (y,z))
by A3, A2, Def20
;
hence
taxi_dist3 . (x,z) <= (taxi_dist3 . (x,y)) + (taxi_dist3 . (y,z))
by A1, A2, A5, Def20; verum