let x, y, z be Element of [:REAL ,REAL :]; :: thesis: 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 by MCART_1:10;
A1: ( x = [x1,x2] & y = [y1,y2] & z = [z1,z2] ) by MCART_1:24;
set d1 = real_dist . x1,z1;
set d2 = real_dist . x1,y1;
set d3 = real_dist . y1,z1;
set d4 = real_dist . x2,z2;
set d5 = real_dist . x2,y2;
set d6 = real_dist . y2,z2;
A2: ((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 A1, Def7
.= (taxi_dist2 . x,y) + (taxi_dist2 . y,z) by A1, Def7 ;
A3: real_dist . x1,z1 <= (real_dist . x1,y1) + (real_dist . y1,z1) by METRIC_1:11;
A4: real_dist . x2,z2 <= (real_dist . x2,y2) + (real_dist . y2,z2) by METRIC_1:11;
taxi_dist2 . x,z = (real_dist . x1,z1) + (real_dist . x2,z2) by A1, Def7;
hence taxi_dist2 . x,z <= (taxi_dist2 . x,y) + (taxi_dist2 . y,z) by A2, A3, A4, XREAL_1:9; :: thesis: verum