for G1 being _Graph
for G2 being Subgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2
for e being set st W1 = W2 & e in (W2 .last()) .edgesInOut() holds
W1 .addEdge e = W2 .addEdge e