theorem :: GLIB_001:62

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 = W ^ <*e,x*> by Lm35;