theorem :: GLIB_001:96

for G being _Graph
for W being Walk of G
for e, x being set st e Joins W .last() ,x,G & not x in W .vertices() holds
card ((W .addEdge e) .vertices()) = (card (W .vertices())) + 1