let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let G1 be addAdjVertexAll of G2,v,V; :: thesis:
assume that
A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A2: ( not G2 is acyclic or ex G3 being Component of G2 ex w1, w2 being Vertex of G3 st
( w1 in V & w2 in V & w1 <> w2 ) ) ; :: thesis:

per cases by A2;

suppose not G2 is acyclic ; :: thesis:

hence not G1 is acyclic ; :: thesis:

end;

suppose ex G3 being Component of G2 ex w1, w2 being Vertex of G3 st
( w1 in V & w2 in V & w1 <> w2 ) ; :: thesis:

then consider G3 being Component of G2, w1, w2 being Vertex of G3 such that
A3: ( w1 in V & w2 in V & w1 <> w2 ) ;
reconsider w1 = w1, w2 = w2 as Vertex of G2 by A3, A1;
the_Vertices_of G3 = G2 .reachableFrom w1 by GLIB_002:33;
then w2 in G2 .reachableFrom w1 ;
then consider W being Walk of G2 such that
A4: W is_Walk_from w1,w2 by GLIB_002:def 5;
reconsider W1 = W as Walk of G1 by GLIB_006:75;
set P = the Path of W1;
W1 is_Walk_from w1,w2 by A4, GLIB_001:19;
then A5: the Path of W1 is_Walk_from w1,w2 by GLIB_001:160;
consider E being set such that
A6: ( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
A7: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e3 being object st e3 Joins v1,v,G1 holds
e1 = e3 ) ) by A1, Def4;
consider e1 being object such that
A8: ( e1 in E & e1 Joins w1,v,G1 ) and
for e3 being object st e3 Joins w1,v,G1 holds
e1 = e3 by A3, A7;
A9: e1 Joins v,w1,G1 by A8, GLIB_000:14;
consider e2 being object such that
A10: ( e2 in E & e2 Joins w2,v,G1 ) and
for e3 being object st e3 Joins w2,v,G1 holds
e2 = e3 by A3, A7;
set P2 = the Path of W1 .addEdge e2;
set P3 = ( the Path of W1 .addEdge e2) .addEdge e1;
A11: ( the Path of W1 .first() = w1 & the Path of W1 .last() = w2 ) by A5, GLIB_001:def 23;
then A12: ( ( the Path of W1 .addEdge e2) .first() = w1 & ( the Path of W1 .addEdge e2) .last() = v ) by A10, GLIB_001:63;
then A13: ( the Path of W1 .addEdge e2) .addEdge e1 is_Walk_from w1,w1 by A9, GLIB_001:63;
A14: not v in the Path of W1 .vertices()

proof

assume v in the Path of W1 .vertices() ; :: thesis:
then v in W1 .vertices() by GLIB_001:163, TARSKI:def 3;
then v in W .vertices() by GLIB_001:98;
then v in the_Vertices_of G2 ;
hence contradiction by A1; :: thesis:

end;

the Path of W1 is open by A3, A11, GLIB_001:def 24;
then A15: the Path of W1 .addEdge e2 is Path-like by A10, A11, A14, GLIB_001:151;
w1 <> v by A1;
then A16: the Path of W1 .addEdge e2 is open by A12, GLIB_001:def 24;
A17: not e1 in ( the Path of W1 .addEdge e2) .edges()

proof

assume A18: e1 in ( the Path of W1 .addEdge e2) .edges() ; :: thesis:
( the Path of W1 .addEdge e2) .edges() = ( the Path of W1 .edges()) \/ {e2} by A10, A11, GLIB_001:111;
then e1 in ( the Path of W1 .edges()) \/ {e2} by A18;

per cases by XBOOLE_0:def 3;

suppose e1 in the Path of W1 .edges() ; :: thesis:

then e1 in W1 .edges() by GLIB_001:163, TARSKI:def 3;
then e1 in W .edges() by GLIB_001:110;
then A19: e1 in the_Edges_of G2 ;
E /\ (the_Edges_of G2) = {} by A6, XBOOLE_0:def 7;
hence contradiction by A8, A19, Lm7; :: thesis:

end;

suppose e1 in {e2} ; :: thesis:

then e1 = e2 by TARSKI:def 1;
then e2 Joins v,w1,G1 by A9;

per cases by A10, GLIB_000:15;

suppose ( w1 = w2 & v = v ) ; :: thesis:

hence contradiction by A3; :: thesis:

end;

suppose ( w1 = v & v = w2 ) ; :: thesis:

hence contradiction by A3; :: thesis:

end;

for n being odd Element of NAT st 1 < n & n <= len ( the Path of W1 .addEdge e2) holds
( the Path of W1 .addEdge e2) . n <> w1

proof

given n being odd Element of NAT such that A20: ( 1 < n & n <= len ( the Path of W1 .addEdge e2) & ( the Path of W1 .addEdge e2) . n = w1 ) ; :: thesis:
( the Path of W1 .addEdge e2) . 1 = w1 by A12, GLIB_001:def 6;
then n = len ( the Path of W1 .addEdge e2) by A20, A15, Lm16, GLIB_001:def 28;
then ( the Path of W1 .addEdge e2) .last() = w1 by A20, GLIB_001:def 7;
then w1 = v by A12;
then v in V by A3;
hence contradiction by A1; :: thesis:

end;

then A21: ( the Path of W1 .addEdge e2) .addEdge e1 is Path-like by A9, A12, A15, A16, A17, GLIB_001:150;
A22: ( the Path of W1 .addEdge e2) .addEdge e1 is closed by A13, GLIB_001:119;
( the Path of W1 .addEdge e2) .addEdge e1 is trivial by A9, A12, GLIB_001:132;
then ( the Path of W1 .addEdge e2) .addEdge e1 is Cycle-like by A21, A22;
hence not G1 is acyclic by GLIB_002:def 2; :: thesis:

end;