let G be _Graph; :: thesis: for W being Walk of G
for e being set st W is Trail-like & e in () .edgesInOut() & not e in W .edges() holds

let W be Walk of G; :: thesis: for e being set st W is Trail-like & e in () .edgesInOut() & not e in W .edges() holds

let e be set ; :: thesis: ( W is Trail-like & e in () .edgesInOut() & not e in W .edges() implies W .addEdge e is Trail-like )
assume that
A1: W is Trail-like and
A2: e in () .edgesInOut() and
A3: not e in W .edges() ; :: thesis:
set W2 = W .addEdge e;
reconsider lenW2 = len (W .addEdge e) as odd Element of NAT ;
A4: e Joins W .last() ,() .adj e,G by ;
now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len (W .addEdge e) holds
let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len (W .addEdge e) implies (W .addEdge e) . m <> (W .addEdge e) . n )
assume that
A5: 1 <= m and
A6: m < n and
A7: n <= len (W .addEdge e) ; :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n
now :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n
per cases ( n <= len W or n > len W ) ;
suppose A8: n <= len W ; :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n
then m <= len W by ;
then m in dom W by ;
then A9: (W .addEdge e) . m = W . m by ;
1 <= n by ;
then n in dom W by ;
then (W .addEdge e) . n = W . n by ;
hence (W .addEdge e) . m <> (W .addEdge e) . n by A1, A5, A6, A8, A9, Lm57; :: thesis: verum
end;
suppose A10: n > len W ; :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n
n < lenW2 by ;
then n + 1 <= len (W .addEdge e) by NAT_1:13;
then (n + 1) - 1 <= (len (W .addEdge e)) - 1 by XREAL_1:13;
then A11: n <= ((len W) + (1 + 1)) - 1 by ;
(len W) + 1 <= n by ;
then A12: n = (len W) + 1 by ;
then A13: (W .addEdge e) . n = e by ;
A14: (m + 1) - 1 <= ((len W) + 1) - 1 by ;
then m in dom W by ;
then (W .addEdge e) . m = W . m by ;
hence (W .addEdge e) . m <> (W .addEdge e) . n by A3, A5, A13, A14, Lm46; :: thesis: verum
end;
end;
end;
hence (W .addEdge e) . m <> (W .addEdge e) . n ; :: thesis: verum
end;
hence W .addEdge e is Trail-like by Lm57; :: thesis: verum