for G being _Graph
for W being vertex-distinct Walk of G
for e, v being object st e Joins W .last() ,v,G & not v in W .vertices() holds
W .addEdge e is vertex-distinct