:: deftheorem defines dist4 METRIC_3:def 9 :
for X, Y, Z, W being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] holds dist4 (x,y) = (dist_cart4 (X,Y,Z,W)) . (x,y);