let M be MetrSpace; MetrStruct(# the carrier of M, the distance of M #) is MetrSpace
now for a, b, c being Element of MetrStruct(# the carrier of M, the distance of M #) holds
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )let a,
b,
c be
Element of
MetrStruct(# the
carrier of
M, the
distance of
M #);
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )reconsider a9 =
a,
b9 =
b,
c9 =
c as
Element of
M ;
A1:
dist (
a,
c) =
the
distance of
M . (
a,
c)
.=
dist (
a9,
c9)
;
A2:
dist (
a,
b) =
the
distance of
M . (
a,
b)
.=
dist (
a9,
b9)
;
hence
(
dist (
a,
b)
= 0 iff
a = b )
by METRIC_1:1, METRIC_1:2;
( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) dist (
b,
a) =
the
distance of
M . (
b,
a)
.=
dist (
b9,
a9)
;
hence
dist (
a,
b)
= dist (
b,
a)
by A2;
dist (a,c) <= (dist (a,b)) + (dist (b,c)) dist (
b,
c) =
the
distance of
M . (
b,
c)
.=
dist (
b9,
c9)
;
hence
dist (
a,
c)
<= (dist (a,b)) + (dist (b,c))
by A2, A1, METRIC_1:4;
verum end;
hence
MetrStruct(# the carrier of M, the distance of M #) is MetrSpace
by METRIC_1:6; verum