let G be _Graph; :: thesis: for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
len (W .addEdge e) = (len W) + 2
let W be Walk of G; :: thesis: for e, x being set st e Joins W .last() ,x,G holds
len (W .addEdge e) = (len W) + 2
let e, x be set ; :: thesis: ( e Joins W .last() ,x,G implies len (W .addEdge e) = (len W) + 2 )
set W2 = G .walkOf ((W .last()),e,((W .last()) .adj e));
assume A1: e Joins W .last() ,x,G ; :: thesis: len (W .addEdge e) = (len W) + 2
then reconsider x9 = x as Vertex of G by GLIB_000:13;
A2: (W .last()) .adj e = x9 by A1, GLIB_000:66;
then (G .walkOf ((W .last()),e,((W .last()) .adj e))) .first() = W .last() by A1, Lm6;
then A3: (len (W .addEdge e)) + 1 = (len W) + (len (G .walkOf ((W .last()),e,((W .last()) .adj e)))) by Lm9;
G .walkOf ((W .last()),e,((W .last()) .adj e)) = <*(W .last()),e,x*> by A1, A2, Def5;
then (len (W .addEdge e)) + 1 = (len W) + 3 by A3, FINSEQ_1:45;
hence len (W .addEdge e) = (len W) + 2 ; :: thesis: verum