:: deftheorem defines dist2S METRIC_3:def 11 :
for X, Y being non empty MetrSpace
for x, y being Element of [: the carrier of X, the carrier of Y:] holds dist2S (x,y) = (dist_cart2S (X,Y)) . (x,y);