theorem Th47: :: GLIB_006:43

for G being _Graph
for W1, W2 being Walk of G
for e being object st W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G holds
ex W3 being Walk of G st W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,W3)