theorem Th25: :: METRIC_3:25

for x, y being Element of [:REAL,REAL,REAL:] holds
( taxi_dist3 . (x,y) = 0 iff x = y )