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