now :: thesis: for x, y, z being Element of MetrStruct(# [:REAL,REAL:],taxi_dist2 #) holds
( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )

let x, y, z be Element of MetrStruct(# [:REAL,REAL:],taxi_dist2 #); :: thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
reconsider x9 = x, y9 = y, z9 = z as Element of [:REAL,REAL:] ;
A1: dist (x,y) = taxi_dist2 . (x9,y9) by METRIC_1:def 1;
hence ( dist (x,y) = 0 iff x = y ) by Th19; :: thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
dist (y,x) = taxi_dist2 . (y9,x9) by METRIC_1:def 1;
hence dist (x,y) = dist (y,x) by A1, Th20; :: thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
( dist (x,z) = taxi_dist2 . (x9,z9) & dist (y,z) = taxi_dist2 . (y9,z9) ) by METRIC_1:def 1;
hence dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th21; :: thesis: verum

end;

hence MetrStruct(# [:REAL,REAL:],taxi_dist2 #) is non empty strict MetrSpace by METRIC_1:6; :: thesis: verum