let G be _Graph; :: thesis: for W being Walk of G
for e, v being set st e Joins W .last() ,v,G & W is Path-like & not v in W .vertices() & ( W is trivial or not W is closed ) holds
W .addEdge e is Path-like
let W be Walk of G; :: thesis: for e, v being set st e Joins W .last() ,v,G & W is Path-like & not v in W .vertices() & ( W is trivial or not W is closed ) holds
W .addEdge e is Path-like
let e, v be set ; :: thesis: ( e Joins W .last() ,v,G & W is Path-like & not v in W .vertices() & ( W is trivial or not W is closed ) implies W .addEdge e is Path-like )
assume A1: ( e Joins W .last() ,v,G & W is Path-like & not v in W .vertices() & ( W is trivial or not W is closed ) ) ; :: thesis: W .addEdge e is Path-like
then A2: not e in W .edges() by Lm48;
for n being odd Element of NAT st 1 < n & n <= len W holds
v <> W . n by A1, Lm45;
hence W .addEdge e is Path-like by A1, A2, Lm65; :: thesis: verum