set Z = MetrStruct(# (M -neighbour),(nbourdist M) #);

now :: thesis: 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) #); :: 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 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; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

end;

hence MetrStruct(# (M -neighbour),(nbourdist M) #) is MetrSpace by METRIC_1:6; :: thesis: verum