:: deftheorem defines MetrSpaceCart2S METRIC_3:def 12 :
for X, Y being non empty MetrSpace holds MetrSpaceCart2S (X,Y) = MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #);