let G be _Graph; :: thesis: for W being Walk of G
for e being set st W is Trail-like & e in (W .last() ) .edgesInOut() & not e in W .edges() holds
W .addEdge e is Trail-like
let W be Walk of G; :: thesis: for e being set st W is Trail-like & e in (W .last() ) .edgesInOut() & not e in W .edges() holds
W .addEdge e is Trail-like
let e be set ; :: thesis: ( W is Trail-like & e in (W .last() ) .edgesInOut() & not e in W .edges() implies W .addEdge e is Trail-like )
assume A1: ( W is Trail-like & e in (W .last() ) .edgesInOut() & not e in W .edges() ) ; :: thesis: W .addEdge e is Trail-like
then A2: e Joins W .last() ,(W .last() ) .adj e,G by GLIB_000:70;
set W2 = W .addEdge e;
reconsider lenW2 = len (W .addEdge e) as odd Element of NAT ;

now

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 A3: ( 1 <= m & m < n & n <= len (W .addEdge e) ) ; :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n

now

per cases ( n <= len W or n > len W ) ;

suppose A4: n <= len W ; :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n

1 <= n by A3, XXREAL_0:2;
then n in dom W by A4, FINSEQ_3:27;
then A5: (W .addEdge e) . n = W . n by A2, Lm38;
m <= len W by A3, A4, XXREAL_0:2;
then m in dom W by A3, FINSEQ_3:27;
then (W .addEdge e) . m = W . m by A2, Lm38;
hence (W .addEdge e) . m <> (W .addEdge e) . n by A1, A3, A4, A5, Lm57; :: thesis: verum

end;

suppose n > len W ; :: thesis: (W .addEdge e) . m <> (W .addEdge e) . n

then A6: (len W) + 1 <= n by NAT_1:13;
n < lenW2 by A3, XXREAL_0:1;
then n + 1 <= len (W .addEdge e) by NAT_1:13;
then (n + 1) - 1 <= (len (W .addEdge e)) - 1 by XREAL_1:15;
then n <= ((len W) + (1 + 1)) - 1 by A2, Lm37;
then A7: n = (len W) + 1 by A6, XXREAL_0:1;
then A8: (W .addEdge e) . n = e by A2, Lm38;
A9: (m + 1) - 1 <= ((len W) + 1) - 1 by A3, A7, NAT_1:13;
then m in dom W by A3, FINSEQ_3:27;
then (W .addEdge e) . m = W . m by A2, Lm38;
hence (W .addEdge e) . m <> (W .addEdge e) . n by A1, A3, A8, A9, 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