theorem Th26: :: METRIC_3:26

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