set Z = MetrStruct(# (M -neighbour),(nbourdist M) #);
now for V, Q, W being Element of MetrStruct(# (M -neighbour),(nbourdist M) #) holds
( ( dist (V,Q) = 0 implies V = Q ) & ( V = Q implies dist (V,Q) = 0 ) & dist (V,Q) = dist (Q,V) & dist (V,W) <= (dist (V,Q)) + (dist (Q,W)) )let V,
Q,
W be
Element of
MetrStruct(#
(M -neighbour),
(nbourdist M) #);
( ( dist (V,Q) = 0 implies V = Q ) & ( V = Q implies dist (V,Q) = 0 ) & dist (V,Q) = dist (Q,V) & dist (V,W) <= (dist (V,Q)) + (dist (Q,W)) )reconsider V9 =
V,
Q9 =
Q,
W9 =
W as
Element of
M -neighbour ;
A1:
dist (
V,
Q)
= (nbourdist M) . (
V9,
Q9)
by METRIC_1:def 1;
hence
(
dist (
V,
Q)
= 0 iff
V = Q )
by Th34;
( dist (V,Q) = dist (Q,V) & dist (V,W) <= (dist (V,Q)) + (dist (Q,W)) )
dist (
Q,
V)
= (nbourdist M) . (
Q9,
V9)
by METRIC_1:def 1;
hence
dist (
V,
Q)
= dist (
Q,
V)
by A1, Th35;
dist (V,W) <= (dist (V,Q)) + (dist (Q,W))
(
dist (
V,
W)
= (nbourdist M) . (
V9,
W9) &
dist (
Q,
W)
= (nbourdist M) . (
Q9,
W9) )
by METRIC_1:def 1;
hence
dist (
V,
W)
<= (dist (V,Q)) + (dist (Q,W))
by A1, Th36;
verum end;
hence
MetrStruct(# (M -neighbour),(nbourdist M) #) is MetrSpace
by METRIC_1:6; verum