set M = MetrStruct(# [: the carrier of X, the carrier of Y, the carrier of Z:],(dist_cart3 (X,Y,Z)) #);
now 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)) #);
( ( 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;
( 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;
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;
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; verum