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