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