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() = (W .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() = (W .vertices()) \/ {x}
let e, x be object ; :: thesis: ( e Joins W .last() ,x,G implies (W .addEdge e) .vertices() = (W .vertices()) \/ {x} )
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: (W .addEdge e) .vertices() = (W .vertices()) \/ {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 (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: for y being object holds
( ( y in (W .vertices()) \/ {(W .last()),x} implies y in (W .vertices()) \/ {x} ) & ( y in (W .vertices()) \/ {x} implies y in (W .vertices()) \/ {(W .last()),x} ) )

let y be object ; :: thesis: ( ( y in (W .vertices()) \/ {(W .last()),x} implies y in (W .vertices()) \/ {x} ) & ( y in (W .vertices()) \/ {x} implies y in (W .vertices()) \/ {(W .last()),x} ) )

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

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

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

per cases ( y in W .vertices() or y in {(W .last()),x} ) by A5, XBOOLE_0:def 3;

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

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

end;

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

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

per cases ( y = W .last() or y = x ) by A6, TARSKI:def 2;

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

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

end;

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

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

end;

end;

end;

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

end;

end;

end;

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

end;

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

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

per cases ( y in W .vertices() or y in {x} ) by A7, XBOOLE_0:def 3;

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

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

end;

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

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: verum

end;

end;

end;

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

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: verum