theorem :: GLIB_001:63

for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x ) by Lm36;