theorem :: GLIB_001:123

for G being _Graph
for W being Walk of G
for e, x, y, z being set st W is directed & W is_Walk_from x,y & e DJoins y,z,G holds
( W .addEdge e is directed & W .addEdge e is_Walk_from x,z ) by Lm52;