:: deftheorem defines MetrSpaceCart3 METRIC_3:def 5 :
for X, Y, Z being non empty MetrSpace holds MetrSpaceCart3 (X,Y,Z) = MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3 (X,Y,Z)) #);