theorem Th44: :: GLIB_006:40

for G being _Graph
for T1 being Trail of G
for 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 T1, 0 holds
not e in (T1 .replaceEdgeWith (e,W3)) .edges()