theorem :: GLIB_001:66

for G being _Graph
for W being Walk of G
for e, x, y, z being object st W is_Walk_from x,y & e Joins y,z,G holds
W .addEdge e is_Walk_from x,z by Lm39;