let x, y be Element of [:REAL ,REAL ,REAL :]; :: thesis: ( taxi_dist3 . x,y = 0 iff x = y )
reconsider x1 = x `1 , x2 = x `2 , x3 = x `3 , y1 = y `1 , y2 = y `2 , y3 = y `3 as Element of REAL ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) by MCART_1:48;
thus ( taxi_dist3 . x,y = 0 implies x = y ) :: thesis: ( x = y implies taxi_dist3 . x,y = 0 )

proof

assume A2: taxi_dist3 . x,y = 0 ; :: thesis: x = y
set d1 = real_dist . x1,y1;
set d2 = real_dist . x2,y2;
set d3 = real_dist . x3,y3;
set d4 = (real_dist . x1,y1) + (real_dist . x2,y2);
A3: ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3) = 0 by A1, A2, Def11;
real_dist . x3,y3 = abs (x3 - y3) by METRIC_1:def 13;
then A4: 0 <= real_dist . x3,y3 by COMPLEX1:132;
real_dist . x2,y2 = abs (x2 - y2) by METRIC_1:def 13;
then A5: 0 <= real_dist . x2,y2 by COMPLEX1:132;
real_dist . x1,y1 = abs (x1 - y1) by METRIC_1:def 13;
then A6: 0 <= real_dist . x1,y1 by COMPLEX1:132;
then A7: 0 + 0 <= (real_dist . x1,y1) + (real_dist . x2,y2) by A5, XREAL_1:9;
then A8: ( (real_dist . x1,y1) + (real_dist . x2,y2) = 0 & real_dist . x3,y3 = 0 ) by A3, A4, XREAL_1:29;
(real_dist . x1,y1) + (real_dist . x2,y2) = 0 by A3, A4, A7, XREAL_1:29;
then A9: ( real_dist . x1,y1 = 0 & real_dist . x2,y2 = 0 ) by A5, A6, XREAL_1:29;
A10: x3 = y3 by A8, METRIC_1:9;
x1 = y1 by A9, METRIC_1:9;
hence x = y by A1, A9, A10, METRIC_1:9; :: thesis: verum

end;

assume A11: x = y ; :: thesis: taxi_dist3 . x,y = 0
then A12: real_dist . x1,y1 = 0 by METRIC_1:9;
A13: real_dist . x2,y2 = 0 by A11, METRIC_1:9;
taxi_dist3 . x,y = ((real_dist . x1,y1) + (real_dist . x2,y2)) + (real_dist . x3,y3) by A1, Def11
.= 0 by A11, A12, A13, METRIC_1:9 ;
hence taxi_dist3 . x,y = 0 ; :: thesis: verum