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;
hence ( dist V,Q = 0 iff V = Q ) by Th54; :: thesis: ( dist V,Q = dist Q,V & dist V,W <= (dist V,Q) + (dist Q,W) )
dist Q,V = (nbourdist M) . Q',V' by METRIC_1:def 1;
hence dist V,Q = dist Q,V by A1, Th55; :: thesis: dist V,W <= (dist V,Q) + (dist Q,W)
( dist V,W = (nbourdist M) . V',W' & dist Q,W = (nbourdist M) . Q',W' ) by METRIC_1:def 1;
hence dist V,W <= (dist V,Q) + (dist Q,W) by A1, Th56; :: thesis: verum

end;

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