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