:: deftheorem Def20 defines taxi_dist3 METRIC_3:def 20 :
for b₁ being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL holds
( b₁ = taxi_dist3 iff for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b₁ . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) );