let M be MetrSpace; :: thesis: MetrStruct(# the carrier of M,the distance of M #) is MetrSpace
now let a,
b,
c be
Element of the
carrier of
MetrStruct(# the
carrier of
M,the
distance of
M #);
:: thesis: ( ( 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 a' =
a,
b' =
b,
c' =
c as
Element of
M ;
A1:
dist a,
b =
the
distance of
M . a,
b
by METRIC_1:def 1
.=
dist a',
b'
by METRIC_1:def 1
;
hence
(
dist a,
b = 0 iff
a = b )
by METRIC_1:1, METRIC_1:2;
:: thesis: ( dist a,b = dist b,a & dist a,c <= (dist a,b) + (dist b,c) ) dist b,
a =
the
distance of
M . b,
a
by METRIC_1:def 1
.=
dist b',
a'
by METRIC_1:def 1
;
hence
dist a,
b = dist b,
a
by A1;
:: thesis: dist a,c <= (dist a,b) + (dist b,c)A2:
dist b,
c =
the
distance of
M . b,
c
by METRIC_1:def 1
.=
dist b',
c'
by METRIC_1:def 1
;
dist a,
c =
the
distance of
M . a,
c
by METRIC_1:def 1
.=
dist a',
c'
by METRIC_1:def 1
;
hence
dist a,
c <= (dist a,b) + (dist b,c)
by A1, A2, METRIC_1:4;
:: thesis: verum end;
hence
MetrStruct(# the carrier of M,the distance of M #) is MetrSpace
by METRIC_1:6; :: thesis: verum