now let x,
y,
z be
Element of
MetrStruct(#
[:REAL ,REAL ,REAL :],
Eukl_dist3 #);
:: 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
[:REAL ,REAL ,REAL :] ;
A1:
dist x,
y = Eukl_dist3 . x',
y'
by METRIC_1:def 1;
A2:
dist x,
z = Eukl_dist3 . x',
z'
by METRIC_1:def 1;
A3:
dist y,
z = Eukl_dist3 . y',
z'
by METRIC_1:def 1;
A4:
dist y,
x = Eukl_dist3 . y',
x'
by METRIC_1:def 1;
thus
(
dist x,
y = 0 iff
x = y )
by A1, Th28;
:: 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, Th29;
:: thesis: dist x,z <= (dist x,y) + (dist y,z)thus
dist x,
z <= (dist x,y) + (dist y,z)
by A1, A2, A3, Th30;
:: thesis: verum end;
hence
MetrStruct(# [:REAL ,REAL ,REAL :],Eukl_dist3 #) is non empty strict MetrSpace
by METRIC_1:6; :: thesis: verum