for G being _Graph
for W1, W3 being Walk of G
for e being object st e Joins W3 .first() ,W3 .last() ,G & not e in W3 .edges() & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 & ( for n, m being even Nat st n in dom W1 & m in dom W1 & W1 . n = e & W1 . m = e holds
n = m ) holds
not e in (W1 .replaceEdgeWith (e,W3)) .edges()