let G be _Graph; :: thesis: for W being Walk of G
for e being object st not e in (W .last()) .edgesInOut() holds
W .addEdge e = W
let W be Walk of G; :: thesis: for e being object st not e in (W .last()) .edgesInOut() holds
W .addEdge e = W
let e be object ; :: thesis: ( not e in (W .last()) .edgesInOut() implies W .addEdge e = W )
set v = the Element of the_Vertices_of G;
A1: e is set by TARSKI:1;
assume not e in (W .last()) .edgesInOut() ; :: thesis: W .addEdge e = W
then A2: not e Joins W .last() ,(W .last()) .adj e,G by A1, GLIB_000:67;
thus W .addEdge e = W .append (G .walkOf ((W .last()),e,((W .last()) .adj e))) by GLIB_001:def 13
.= W .append (G .walkOf the Element of the_Vertices_of G) by A2, GLIB_001:def 5
.= W by GLIB_001:130 ; :: thesis: verum