:: deftheorem Def6 defines .replaceEdgeWith GLIB_006:def 6 :
for G being _Graph
for W1, W3 being Walk of G
for e being object holds
( ( e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 implies W1 .replaceEdgeWith (e,W3) = W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3) ) & ( ( not e Joins W3 .first() ,W3 .last() ,G or not G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 ) implies W1 .replaceEdgeWith (e,W3) = W1 ) );