let G be _Graph; :: thesis:
let T1 be Trail of G; :: thesis:
let W3 be Walk of G; :: thesis:
let e be object ; :: thesis:
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:
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:
assume A4: ( n in dom T1 & m in dom T1 & T1 . n = e & T1 . m = e ) ; :: thesis:
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 by XXREAL_0:1;

suppose n < m ; :: thesis:

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

end;

suppose n = m ; :: thesis:

hence n = m ; :: thesis:

end;

suppose n > m ; :: thesis:

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

end;

end;

end;

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