set Z = MetrStruct(# (M -neighbour ),(nbourdist M) #);
now let V,
Q,
W be
Element of
MetrStruct(#
(M -neighbour ),
(nbourdist M) #);
:: thesis: ( ( 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 V' =
V,
Q' =
Q,
W' =
W as
Element of
M -neighbour ;
A1:
dist V,
Q = (nbourdist M) . V',
Q'
by METRIC_1:def 1;
A2:
dist Q,
V = (nbourdist M) . Q',
V'
by METRIC_1:def 1;
A3:
dist V,
W = (nbourdist M) . V',
W'
by METRIC_1:def 1;
A4:
dist Q,
W = (nbourdist M) . Q',
W'
by METRIC_1:def 1;
thus
(
dist V,
Q = 0 iff
V = Q )
by A1, Th54;
:: thesis: ( dist V,Q = dist Q,V & dist V,W <= (dist V,Q) + (dist Q,W) )thus
dist V,
Q = dist Q,
V
by A1, A2, Th55;
:: thesis: dist V,W <= (dist V,Q) + (dist Q,W)thus
dist V,
W <= (dist V,Q) + (dist Q,W)
by A1, A3, A4, Th56;
:: thesis: verum end;
hence
MetrStruct(# (M -neighbour ),(nbourdist M) #) is MetrSpace
by METRIC_1:6; :: thesis: verum