let G2 be _Graph; :: thesis:
let v1, v2 be Vertex of G2; :: thesis:
let e be object ; :: thesis:
let G1 be addEdge of G2,v1,e,v2; :: thesis:
assume that
A1: G2 is acyclic and
A2: not v2 in G2 .reachableFrom v1 ; :: thesis:

suppose A3: ( v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis:

for W1 being Walk of G1 holds not W1 is Cycle-like

given W1 being Walk of G1 such that A4: W1 is Cycle-like ; :: thesis:
A5: G2 is Subgraph of G1 by Th61;
A6: the_Vertices_of G1 = the_Vertices_of G2 by A3, Def11;
then A7: W1 .vertices() c= the_Vertices_of G2 ;

suppose W1 .edges() c= the_Edges_of G2 ; :: thesis:

then reconsider W = W1 as Walk of G2 by A5, A7, GLIB_001:170;
W is Cycle-like by A4, A5, Th58;
hence contradiction by A1, GLIB_002:def 2; :: thesis:

end;

suppose not W1 .edges() c= the_Edges_of G2 ; :: thesis:

then consider e1 being object such that
A8: ( e1 in W1 .edges() & not e1 in the_Edges_of G2 ) by TARSKI:def 3;
the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A3, Def11;
then e1 in {e} by A8, XBOOLE_0:def 3;
then A10: e1 = e by TARSKI:def 1;
then e1 DJoins v1,v2,G1 by A3, Th109;
then e1 Joins v1,v2,G1 by GLIB_000:16;
then consider W2 being Walk of G1 such that
A11: ( W2 is_Walk_from v1,v2 & not e1 in W2 .edges() ) by A8, A4, GLIB_001:157;
W2 .edges() c= the_Edges_of G1 ;
then W2 .edges() c= (the_Edges_of G2) \/ {e} by A3, Def11;
then A12: W2 .edges() c= the_Edges_of G2 by A11, A10, ZFMISC_1:135;
W2 .vertices() c= the_Vertices_of G2 by A6;
then reconsider W = W2 as Walk of G2 by A5, A12, GLIB_001:170;
reconsider w1 = v1, w2 = v2 as Vertex of G2 ;
W is_Walk_from w1,w2 by A11, GLIB_001:19;
hence contradiction by A2, GLIB_002:def 5; :: thesis:

end;

end;

end;

hence G1 is acyclic by GLIB_002:def 2; :: thesis:

end;

suppose ( not v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or e in the_Edges_of G2 ) ; :: thesis:

then G1 == G2 by Def11;
hence G1 is acyclic by A1, GLIB_002:44; :: thesis:

end;

end;