now :: thesis: for x, y, z being Element of MetrStruct(# [: the carrier of X, the carrier of Y:],(dist_cart2S (X,Y)) #) 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:],(dist_cart2S (X,Y)) #); :: 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:] ;
A1: dist (x,y) = (dist_cart2S (X,Y)) . (x9,y9) by METRIC_1:def 1;
hence ( dist (x,y) = 0 iff x = y ) by Th10; :: thesis: ( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
dist (y,x) = (dist_cart2S (X,Y)) . (y9,x9) by METRIC_1:def 1;
hence dist (x,y) = dist (y,x) by A1, Th11; :: thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
( dist (x,z) = (dist_cart2S (X,Y)) . (x9,z9) & dist (y,z) = (dist_cart2S (X,Y)) . (y9,z9) ) by METRIC_1:def 1;
hence dist (x,z) <= (dist (x,y)) + (dist (y,z)) by A1, Th13; :: thesis: verum

end;

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