theorem Th32: :: GLIBPRE1:32

for G being _Graph
for W1 being Walk of G
for e, x, y being object st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Path of G st
( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) )