theorem :: GLIB_001:64

for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
len (W .addEdge e) = (len W) + 2 by Lm37;