let G2 be _Graph; :: thesis:
let v1, e be object ; :: thesis:
let v2 be Vertex of G2; :: thesis:
let G1 be addAdjVertex of G2,v1,e,v2; :: thesis:
let W be Walk of G1; :: thesis:
assume that
A1: ( not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 ) and
A2: ( ( not e in W .edges() & W is V5() ) or not v1 in W .vertices() ) ; :: thesis:
reconsider w = v1, e1 = e as set by TARSKI:1;

per cases by A2;

suppose A3: ( not e in W .edges() & W is V5() ) ; :: thesis:

consider G3 being addVertex of G2,v1 such that
A4: G1 is addEdge of G3,v1,e,v2 by A1, Th130;
A5: not e in the_Edges_of G3 by A1, Def10;
A6: v2 is Vertex of G3 by Th72;
v1 is Vertex of G3 by Th98;
then G3 is removeEdge of G1,e1 by A4, A5, A6, Th112;
then reconsider W3 = W as Walk of G3 by A3, GLIB_001:172;
W3 .vertices() misses {v1} \ (the_Vertices_of G2) by A3, Th94;
hence W is Walk of G2 by Th95; :: thesis:

end;

suppose A7: not v1 in W .vertices() ; :: thesis:

reconsider G3 = G2 as removeVertex of G1,w by A1, Th142;
reconsider w = w as Vertex of G1 by A1, Th134;
A8: not w in W .vertices() by A7;
not G1 is _trivial by A1, Th148;
then W is Walk of G3 by A8, GLIB_001:171;
hence W is Walk of G2 ; :: thesis:

end;

end;