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) .vertices() = (W .vertices() ) \/ {x}
let W be Walk of G; :: thesis: for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .vertices() = (W .vertices() ) \/ {x}
let e, x be set ; :: 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 x' = x as Vertex of G by GLIB_000:16;
A2: (W .last() ) .adj e = x' by A1, GLIB_000:69;
then (G .walkOf (W .last() ),e,((W .last() ) .adj e)) .first() = W .last() by A1, Th16;
then A3: (W .addEdge e) .vertices() = (W .vertices() ) \/ ((G .walkOf (W .last() ),e,((W .last() ) .adj e)) .vertices() ) by Th94;
A4: (G .walkOf (W .last() ),e,((W .last() ) .adj e)) .vertices() = {(W .last() ),x} by A1, A2, Th92;

now

let y be set ; :: 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

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

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 Th89;
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

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;

hence (W .addEdge e) .vertices() = (W .vertices() ) \/ {x} by A3, A4, TARSKI:2; :: thesis: verum