for G being _Graph
for W1 being Walk of G
for e, x, y being set st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )