let G be _Graph; :: thesis:
let W be Walk of G; :: thesis:
let e, x be object ; :: thesis:
set W2 = G .walkOf ((W .last()),e,((W .last()) .adj e));
set W3 = W .addEdge e;
set WV = W .vertices() ;
assume A1: e Joins W .last() ,x,G ; :: thesis:
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, Th14;
then A3: (W .addEdge e) .vertices() = (W .vertices()) \/ ((G .walkOf ((W .last()),e,((W .last()) .adj e))) .vertices()) by Th91;

A4: now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume A5: y in (W .vertices()) \/ {(W .last()),x} ; :: thesis:

now :: thesis:

per cases by A5, XBOOLE_0:def 3;

suppose y in W .vertices() ; :: thesis:

hence y in (W .vertices()) \/ {x} by XBOOLE_0:def 3; :: thesis:

end;

suppose A6: y in {(W .last()),x} ; :: thesis:

now :: thesis:

per cases by A6, TARSKI:def 2;

suppose y = W .last() ; :: thesis:

then y in W .vertices() by Th86;
hence y in (W .vertices()) \/ {x} by XBOOLE_0:def 3; :: thesis:

end;

suppose y = x ; :: thesis:

then y in {x} by TARSKI:def 1;
hence y in (W .vertices()) \/ {x} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

hence y in (W .vertices()) \/ {x} ; :: thesis:

end;

end;

end;

hence y in (W .vertices()) \/ {x} ; :: thesis:

end;

assume A7: y in (W .vertices()) \/ {x} ; :: thesis:

now :: thesis:

per cases by A7, XBOOLE_0:def 3;

suppose y in W .vertices() ; :: thesis:

hence y in (W .vertices()) \/ {(W .last()),x} by XBOOLE_0:def 3; :: thesis:

end;

suppose y in {x} ; :: thesis:

then y = x by TARSKI:def 1;
then y in {(W .last()),x} by TARSKI:def 2;
hence y in (W .vertices()) \/ {(W .last()),x} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

hence y in (W .vertices()) \/ {(W .last()),x} ; :: thesis:

end;

(G .walkOf ((W .last()),e,((W .last()) .adj e))) .vertices() = {(W .last()),x} by A1, A2, Th89;
hence (W .addEdge e) .vertices() = (W .vertices()) \/ {x} by A3, A4, TARSKI:2; :: thesis: