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

now :: thesis: for x, y, z being Element of MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3 (X,Y,Z)) #) 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:],(dist_cart3 (X,Y,Z)) #); :: 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)) )
A1: dist (x,y) = (dist_cart3 (X,Y,Z)) . (x,y) by METRIC_1:def 1;
hence ( dist (x,y) = 0 iff x = y ) by Th4; :: thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
dist (y,x) = (dist_cart3 (X,Y,Z)) . (y,x) by METRIC_1:def 1;
hence dist (x,y) = dist (y,x) by A1, Th5; :: thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
( dist (x,z) = (dist_cart3 (X,Y,Z)) . (x,z) & dist (y,z) = (dist_cart3 (X,Y,Z)) . (y,z) ) by METRIC_1:def 1;
hence dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th6; :: thesis: verum

end;

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