now for x, y, z being Element of MetrStruct(# [:REAL,REAL:],Eukl_dist2 #) 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(#
[:REAL,REAL:],
Eukl_dist2 #);
( ( 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
[:REAL,REAL:] ;
A1:
dist (
x,
y)
= Eukl_dist2 . (
x9,
y9)
by METRIC_1:def 1;
hence
(
dist (
x,
y)
= 0 iff
x = y )
by Th22;
( dist (x,y) = dist (y,x) & dist (x,z) <= (dist (x,y)) + (dist (y,z)) )
dist (
y,
x)
= Eukl_dist2 . (
y9,
x9)
by METRIC_1:def 1;
hence
dist (
x,
y)
= dist (
y,
x)
by A1, Th23;
dist (x,z) <= (dist (x,y)) + (dist (y,z))
(
dist (
x,
z)
= Eukl_dist2 . (
x9,
z9) &
dist (
y,
z)
= Eukl_dist2 . (
y9,
z9) )
by METRIC_1:def 1;
hence
dist (
x,
z)
<= (dist (x,y)) + (dist (y,z))
by A1, Th24;
verum end;
hence
MetrStruct(# [:REAL,REAL:],Eukl_dist2 #) is non empty strict MetrSpace
by METRIC_1:6; verum