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:62;
then A1: e Joins W .last() ,(W .last()) .adj e,G by GLIB_000:67;
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