theorem Th21: :: METRIC_3:21

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