now let x,
y,
z be
Element of
MetrStruct(#
[:the carrier of X,the carrier of Y,the carrier of Z:],
(dist_cart3S 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) )reconsider x' =
x,
y' =
y,
z' =
z as
Element of
[:the carrier of X,the carrier of Y,the carrier of Z:] ;
A1:
dist x,
y = (dist_cart3S X,Y,Z) . x',
y'
by METRIC_1:def 1;
A2:
dist x,
z = (dist_cart3S X,Y,Z) . x',
z'
by METRIC_1:def 1;
A3:
dist y,
z = (dist_cart3S X,Y,Z) . y',
z'
by METRIC_1:def 1;
A4:
dist y,
x = (dist_cart3S X,Y,Z) . y',
x'
by METRIC_1:def 1;
thus
(
dist x,
y = 0 iff
x = y )
by A1, Th10;
:: 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, Th11;
:: thesis: dist x,z <= (dist x,y) + (dist y,z)thus
dist x,
z <= (dist x,y) + (dist y,z)
by A1, A2, A3, Th16;
:: thesis: verum end;
hence
MetrStruct(# [:the carrier of X,the carrier of Y,the carrier of Z:],(dist_cart3S X,Y,Z) #) is non empty strict MetrSpace
by METRIC_1:6; :: thesis: verum