let x, y, z be Element of [:REAL,REAL:]; taxi_dist2 . (x,z) <= (taxi_dist2 . (x,y)) + (taxi_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:
y = [y1,y2]
;
set d5 = real_dist . (x2,y2);
set d6 = real_dist . (y2,z2);
set d3 = real_dist . (y1,z1);
set d4 = real_dist . (x2,z2);
set d1 = real_dist . (x1,z1);
set d2 = real_dist . (x1,y1);
A2:
z = [z1,z2]
;
A3:
x = [x1,x2]
;
then A4:
taxi_dist2 . (x,z) = (real_dist . (x1,z1)) + (real_dist . (x2,z2))
by A2, Def16;
A5:
( 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;
((real_dist . (x1,y1)) + (real_dist . (y1,z1))) + ((real_dist . (x2,y2)) + (real_dist . (y2,z2))) =
((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + ((real_dist . (y1,z1)) + (real_dist . (y2,z2)))
.=
(taxi_dist2 . (x,y)) + ((real_dist . (y1,z1)) + (real_dist . (y2,z2)))
by A3, A1, Def16
.=
(taxi_dist2 . (x,y)) + (taxi_dist2 . (y,z))
by A1, A2, Def16
;
hence
taxi_dist2 . (x,z) <= (taxi_dist2 . (x,y)) + (taxi_dist2 . (y,z))
by A5, A4, XREAL_1:7; verum