let G be _Graph; for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
(W .addEdge e) .edges() = (W .edges()) \/ {e}
let W be Walk of G; for e, x being object st e Joins W .last() ,x,G holds
(W .addEdge e) .edges() = (W .edges()) \/ {e}
let e, x be object ; ( 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
; (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 Th14;
(G .walkOf ((W .last()),e,((W .last()) .adj e))) .edges() = {e}
by A1, Th106;
hence
(W .addEdge e) .edges() = (W .edges()) \/ {e}
by A2, Th100; verum