let G be _Graph; :: thesis: for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .edges() = (W .edges() ) \/ {e}
let W be Walk of G; :: thesis: for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .edges() = (W .edges() ) \/ {e}
let e, x be set ; :: thesis: ( e Joins W .last() ,x,G implies (W .addEdge e) .edges() = (W .edges() ) \/ {e} )
set WB = G .walkOf (W .last() ),e,((W .last() ) .adj e);
assume e Joins W .last() ,x,G ; :: thesis: (W .addEdge e) .edges() = (W .edges() ) \/ {e}
then e in (W .last() ) .edgesInOut() by GLIB_000:65;
then A1: e Joins W .last() ,(W .last() ) .adj e,G by GLIB_000:70;
then A2: (G .walkOf (W .last() ),e,((W .last() ) .adj e)) .first() = W .last() by Th16;
(G .walkOf (W .last() ),e,((W .last() ) .adj e)) .edges() = {e} by A1, Th109;
hence (W .addEdge e) .edges() = (W .edges() ) \/ {e} by A2, Th103; :: thesis: verum