set M = MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],(dist_cart4 (X,Y,Z,W)) #);

now :: thesis: for x, y, z being Element of MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],(dist_cart4 (X,Y,Z,W)) #) holds
( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )

let x, y, z be Element of MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],(dist_cart4 (X,Y,Z,W)) #); :: thesis: ( ( dist (x,y) = 0 implies x = y ) & ( x = y implies dist (x,y) = 0 ) & dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
reconsider x9 = x, y9 = y, z9 = z as Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] ;
A1: dist (x,y) = (dist_cart4 (X,Y,Z,W)) . (x9,y9) by METRIC_1:def 1;
hence ( dist (x,y) = 0 iff x = y ) by Th7; :: thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
dist (y,x) = (dist_cart4 (X,Y,Z,W)) . (y9,x9) by METRIC_1:def 1;
hence dist (x,y) = dist (y,x) by A1, Th8; :: thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
( dist (x,z) = (dist_cart4 (X,Y,Z,W)) . (x9,z9) & dist (y,z) = (dist_cart4 (X,Y,Z,W)) . (y9,z9) ) by METRIC_1:def 1;
hence dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th9; :: thesis: verum

end;

hence MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],(dist_cart4 (X,Y,Z,W)) #) is non empty strict MetrSpace by METRIC_1:6; :: thesis: verum