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) .vertices() = () \/ {x}

let W be Walk of G; :: thesis: for e, x being object st e Joins W .last() ,x,G holds
(W .addEdge e) .vertices() = () \/ {x}

let e, x be object ; :: thesis: ( e Joins W .last() ,x,G implies (W .addEdge e) .vertices() = () \/ {x} )
set W2 = G .walkOf ((),e,(() .adj e));
set W3 = W .addEdge e;
set WV = W .vertices() ;
assume A1: e Joins W .last() ,x,G ; :: thesis: (W .addEdge e) .vertices() = () \/ {x}
then reconsider x9 = x as Vertex of G by GLIB_000:13;
A2: (W .last()) .adj e = x9 by ;
then (G .walkOf ((),e,(() .adj e))) .first() = W .last() by ;
then A3: (W .addEdge e) .vertices() = () \/ ((G .walkOf ((),e,(() .adj e))) .vertices()) by Th91;
A4: now :: thesis: for y being object holds
( ( y in () \/ {(),x} implies y in () \/ {x} ) & ( y in () \/ {x} implies y in () \/ {(),x} ) )
let y be object ; :: thesis: ( ( y in () \/ {(),x} implies y in () \/ {x} ) & ( y in () \/ {x} implies y in () \/ {(),x} ) )
hereby :: thesis: ( y in () \/ {x} implies y in () \/ {(),x} ) end;
assume A7: y in () \/ {x} ; :: thesis: y in () \/ {(),x}
now :: thesis: y in () \/ {(),x}end;
hence y in () \/ {(),x} ; :: thesis: verum
end;
(G .walkOf ((),e,(() .adj e))) .vertices() = {(),x} by A1, A2, Th89;
hence (W .addEdge e) .vertices() = () \/ {x} by ; :: thesis: verum