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) .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 set 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 set ; :: 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 x' = x as Vertex of G by GLIB_000:16;
(W .last() ) .adj e = x' by A1, GLIB_000:69;
then ( (G .walkOf (W .last() ),e,((W .last() ) .adj e)) .first() = W .last() & (G .walkOf (W .last() ),e,((W .last() ) .adj e)) .last() = x ) by A1, Lm6;
hence ( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x ) by Lm11; :: thesis: verum