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) #);
MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:],(dist_cart4 X,Y,Z,W) #) is MetrSpace

proof

now

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 x' = x, y' = y, z' = 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) . x',y' by METRIC_1:def 1;
A2: dist x,z = (dist_cart4 X,Y,Z,W) . x',z' by METRIC_1:def 1;
A3: dist y,z = (dist_cart4 X,Y,Z,W) . y',z' by METRIC_1:def 1;
A4: dist y,x = (dist_cart4 X,Y,Z,W) . y',x' by METRIC_1:def 1;
thus ( dist x,y = 0 iff x = y ) by A1, Th19; :: thesis: ( dist x,y = dist y,x & dist x,z <= (dist x,y) + (dist y,z) )
thus dist x,y = dist y,x by A1, A4, Th20; :: thesis: dist x,z <= (dist x,y) + (dist y,z)
thus dist x,z <= (dist x,y) + (dist y,z) by A1, A2, A3, Th21; :: 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 MetrSpace by METRIC_1:6; :: 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 ; :: thesis: verum