let G be _Graph; :: thesis: for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x )
let W be Walk of G; :: thesis: for e, x being object st e Joins W .last() ,x,G holds
( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x )
let e, x be object ; :: thesis: ( e Joins W .last() ,x,G implies ( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x ) )
set W2 = G .walkOf ((W .last()),e,((W .last()) .adj e));
assume A1: e Joins W .last() ,x,G ; :: thesis: ( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x )
then reconsider x9 = x as Vertex of G by GLIB_000:13;
A2: (W .last()) .adj e = x9 by A1, GLIB_000:66;
then A3: (G .walkOf ((W .last()),e,((W .last()) .adj e))) .last() = x by A1, Lm6;
(G .walkOf ((W .last()),e,((W .last()) .adj e))) .first() = W .last() by A1, A2, Lm6;
hence ( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x ) by A3, Lm11; :: thesis: verum