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 ;

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; :: thesis: verum

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; :: thesis: verum