theorem Th27: :: METRIC_3:27

for x, y, z being Element of [:REAL,REAL,REAL:] holds taxi_dist3 . (x,z) <= (taxi_dist3 . (x,y)) + (taxi_dist3 . (y,z))