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