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() & ( 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() & ( 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() & ( 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: ( 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

for e, v being object st e Joins W .last() ,v,G & W is Path-like & not v in W .vertices() & ( 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() & ( 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() & ( 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: ( 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