let G be _Graph; :: thesis: 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()
let T1 be Trail of G; :: thesis: 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()
let W3 be Walk of G; :: thesis: 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()
let e be object ; :: thesis: ( 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 implies not e in (T1 .replaceEdgeWith (e,W3)) .edges() )
assume that
A1: e Joins W3 .first() ,W3 .last() ,G and
A2: not e in W3 .edges() and
A3: G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of T1, 0 ; :: thesis: not e in (T1 .replaceEdgeWith (e,W3)) .edges()
for n, m being even Nat st n in dom T1 & m in dom T1 & T1 . n = e & T1 . m = e holds
n = m

proof

let n, m be even Nat; :: thesis: ( n in dom T1 & m in dom T1 & T1 . n = e & T1 . m = e implies n = m )
assume A4: ( n in dom T1 & m in dom T1 & T1 . n = e & T1 . m = e ) ; :: thesis: n = m
then A5: ( 1 <= n & n <= len T1 & 1 <= m & m <= len T1 ) by FINSEQ_3:25;
reconsider n = n, m = m as even Element of NAT by ORDINAL1:def 12;

per cases ( n < m or n = m or n > m ) by XXREAL_0:1;

suppose n < m ; :: thesis: n = m

hence n = m by A4, A5, GLIB_001:138; :: thesis: verum

end;

suppose n = m ; :: thesis: n = m

hence n = m ; :: thesis: verum

end;

suppose n > m ; :: thesis: n = m

hence n = m by A4, A5, GLIB_001:138; :: thesis: verum

end;

end;

end;

hence not e in (T1 .replaceEdgeWith (e,W3)) .edges() by A1, A2, A3, Th43; :: thesis: verum