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: G2 is acyclic and
A3: for G3 being Component of G2
for w1, w2 being Vertex of G3 st w1 in V & w2 in V holds
w1 = w2 ; :: thesis:
consider E being set such that
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
A4: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by A1, Def4;
for W being Walk of G1 holds not W is Cycle-like

proof

given C being Walk of G1 such that A5: C is Cycle-like ; :: thesis:
A6: ( C is closed & C is Path-like ) by A5;
set v1 = C .first() ;
A7: C .first() = C .last() by A6, GLIB_001:def 24;

per cases ;

suppose A8: C .first() <> v ; :: thesis:

then A9: not C .first() in {v} by TARSKI:def 1;
A10: the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A1, Def4;
then reconsider v1 = C .first() as Vertex of G2 by A9, XBOOLE_0:def 3;
set G3 = the inducedSubgraph of G2,(G2 .reachableFrom v1);

per cases ;

suppose C .vertices() c= G2 .reachableFrom v1 ; :: thesis:

then A11: C .vertices() c= the_Vertices_of G2 by XBOOLE_1:1;
then A12: C .edges() c= the_Edges_of G2 by Th65;
G2 is Subgraph of G1 by GLIB_006:57;
then reconsider C2 = C as Walk of G2 by A11, A12, GLIB_001:170;
C2 is Cycle-like by A5, GLIB_006:24;
hence contradiction by A2, GLIB_002:def 2; :: thesis:

end;

suppose not C .vertices() c= G2 .reachableFrom v1 ; :: thesis:

then consider v2 being object such that
A13: ( v2 in C .vertices() & not v2 in G2 .reachableFrom v1 ) by TARSKI:def 3;
reconsider v2 = v2 as Vertex of G1 by A13;
consider n being odd Element of NAT such that
A14: n <= len C and
A15: C . n = v2 by A13, GLIB_001:87;
A16: ( 1 < n & n < len C )

proof

thus 1 < n :: thesis:

proof

assume A17: 1 >= n ; :: thesis:
1 <= n by ABIAN:12;
then n = 1 by A17, XXREAL_0:1;
then v2 = v1 by A15, GLIB_001:def 6;
hence contradiction by A13, GLIB_002:9; :: thesis:

end;

assume n >= len C ; :: thesis:
then n = len C by A14, XXREAL_0:1;
then v2 = v1 by A7, A15, GLIB_001:def 7;
hence contradiction by A13, GLIB_002:9; :: thesis:

end;

per cases ;

suppose A18: v2 <> v ; :: thesis:

then not v2 in {v} by TARSKI:def 1;
then reconsider v2 = v2 as Vertex of G2 by A10, XBOOLE_0:def 3;
set P1 = C .cut (1,n);
set P2 = C .cut (n,(len C));
A19: 1 is odd Element of NAT by Lm16;
A20: ( 1 <= n & n <= len C ) by ABIAN:12, A14;
A21: ( n <= len C & len C <= len C ) by A14;
A22: (len (C .cut (1,n))) + 1 = n + 1 by A20, A19, GLIB_001:36;
A23: (len (C .cut (n,(len C)))) + n = (len C) + 1 by A21, GLIB_001:36;
( not v in (C .cut (1,n)) .vertices() or not v in (C .cut (n,(len C))) .vertices() )

proof

assume v in (C .cut (1,n)) .vertices() ; :: thesis:
then consider m being odd Element of NAT such that
A24: ( m <= len (C .cut (1,n)) & (C .cut (1,n)) . m = v ) by GLIB_001:87;
reconsider m1 = m -' 1 as Element of NAT ;
A25: m1 + 1 = m by Lm14;
m1 < len (C .cut (1,n)) by A24, Lm14;
then A26: C . (1 + m1) = v by A19, A20, A24, A25, GLIB_001:36;
assume v in (C .cut (n,(len C))) .vertices() ; :: thesis:
then consider k being odd Element of NAT such that
A27: ( k <= len (C .cut (n,(len C))) & (C .cut (n,(len C))) . k = v ) by GLIB_001:87;
A28: k < len (C .cut (n,(len C)))

proof

assume k >= len (C .cut (n,(len C))) ; :: thesis:
then A29: k = len (C .cut (n,(len C))) by A27, XXREAL_0:1;
v1 = C . (len C) by A7, GLIB_001:def 7
.= (C .cut (n,(len C))) .last() by A21, GLIB_001:37
.= v by A27, A29, GLIB_001:def 7 ;
hence contradiction by A8; :: thesis:

end;

reconsider k1 = k -' 1 as Element of NAT ;
A30: k1 + 1 = k by Lm14;
k1 < len (C .cut (n,(len C))) by A27, Lm14;
then C . (n + k1) = v by A21, A27, A30, GLIB_001:36;
then A31: C . m = C . (n + k1) by A25, A26;
reconsider nk = n + k1 as odd Element of NAT by Lm15;
A32: 1 <= k1

proof

A33: 1 <= k by ABIAN:12;
1 < k

proof

assume 1 >= k ; :: thesis:
then k = 1 by A33, XXREAL_0:1;
then A34: (C .cut (n,(len C))) .first() = v by A27, GLIB_001:def 6;
(C .cut (n,(len C))) .first() = v2 by A15, A21, GLIB_001:37;
hence contradiction by A34, A18; :: thesis:

end;

hence 1 <= k1 by NAT_D:49; :: thesis:

end;

m < (len (C .cut (1,n))) + 1 by A24, NAT_1:13;
then A35: m < n + 1 by A22;
n + 1 <= n + k1 by A32, XREAL_1:6;
then A36: m < nk by A35, XXREAL_0:2;
A37: 1 <= k by ABIAN:12;
k + n <= (len C) + 1 by A27, A23, XREAL_1:6;
then (k + n) - 1 <= ((len C) + 1) - 1 by XREAL_1:9;
then n + (k - 1) <= len C ;
then n + k1 <= len C by A37, XREAL_1:233;
then ( m = 1 & nk = len C ) by A6, A31, GLIB_001:def 28, A36;
hence contradiction by A28, A30, A23; :: thesis:

end;

per cases ;

suppose not v in (C .cut (1,n)) .vertices() ; :: thesis:

then reconsider P3 = C .cut (1,n) as Walk of G2 by A1, Th64;
C .cut (1,n) is_Walk_from C . 1,C . n by A20, A19, GLIB_001:37;
then C .cut (1,n) is_Walk_from v1,v2 by A15, GLIB_001:def 6;
then P3 is_Walk_from v1,v2 by GLIB_001:19;
then v2 in G2 .reachableFrom v1 by GLIB_002:def 5;
hence contradiction by A13; :: thesis:

end;

suppose not v in (C .cut (n,(len C))) .vertices() ; :: thesis:

then reconsider P3 = C .cut (n,(len C)) as Walk of G2 by A1, Th64;
C .cut (n,(len C)) is_Walk_from C . n,C . (len C) by A21, GLIB_001:37;
then C .cut (n,(len C)) is_Walk_from v2,v1 by A15, A7, GLIB_001:def 7;
then P3 is_Walk_from v2,v1 by GLIB_001:19;
then P3 .reverse() is_Walk_from v1,v2 by GLIB_001:23;
hence contradiction by A13, GLIB_002:def 5; :: thesis:

end;

suppose A38: v2 = v ; :: thesis:

reconsider m = n - 2 as odd Element of NAT by A16, Lm13;
set P1 = C .cut (1,m);
set P2 = C .cut ((n + 2),(len C));
n - 2 <= (len C) - 0 by A14, XREAL_1:13;
then A39: ( 1 <= m & m <= len C ) by ABIAN:12;
A40: ( n + 2 <= len C & len C <= len C ) by A16, GLIB_001:1;
A41: (len (C .cut (1,m))) + 1 = m + 1 by A39, Lm16, GLIB_001:36;
A42: (len (C .cut ((n + 2),(len C)))) + (n + 2) = (len C) + 1 by A40, GLIB_001:36;
A43: ( not v in (C .cut (1,m)) .vertices() & not v in (C .cut ((n + 2),(len C))) .vertices() )

proof

assume ( v in (C .cut (1,m)) .vertices() or v in (C .cut ((n + 2),(len C))) .vertices() ) ; :: thesis:

per cases ;

suppose v in (C .cut (1,m)) .vertices() ; :: thesis:

then consider k being odd Element of NAT such that
A44: ( k <= len (C .cut (1,m)) & (C .cut (1,m)) . k = v ) by GLIB_001:87;
reconsider k1 = k -' 1 as Element of NAT ;
k1 < len (C .cut (1,m)) by A44, Lm14;
then (C .cut (1,m)) . (k1 + 1) = C . (1 + k1) by A39, Lm16, GLIB_001:36;
then (C .cut (1,m)) . k = C . (k1 + 1) by Lm14;
then (C .cut (1,m)) . k = C . k by Lm14;
then A45: C . k = C . n by A38, A15, A44;
n - 2 < n - 0 by XREAL_1:15;
then A46: m < n ;
k <= m by A44, A41;
then ( k < n & n <= len C ) by A14, A46, XXREAL_0:2;
then n = len C by A5, A45, GLIB_001:def 28;
hence contradiction by A16; :: thesis:

end;

suppose v in (C .cut ((n + 2),(len C))) .vertices() ; :: thesis:

then consider k being odd Element of NAT such that
A47: ( k <= len (C .cut ((n + 2),(len C))) & (C .cut ((n + 2),(len C))) . k = v ) by GLIB_001:87;
reconsider k1 = k -' 1 as Element of NAT ;
k1 < len (C .cut ((n + 2),(len C))) by A47, Lm14;
then (C .cut ((n + 2),(len C))) . (k1 + 1) = C . ((n + 2) + k1) by A40, GLIB_001:36;
then (C .cut ((n + 2),(len C))) . k = C . ((n + (k1 + 1)) + 1) by Lm14;
then A48: (C .cut ((n + 2),(len C))) . k = C . ((n + k) + 1) by Lm14;
reconsider nk = (n + k) + 1 as odd Element of NAT ;
A49: C . nk = C . n by A38, A15, A47, A48;
( n < nk & nk <= len C )

proof

n < n + 1 by NAT_1:13;
then n + 0 < (n + 1) + k by XREAL_1:8;
hence n < nk ; :: thesis:
(len (C .cut ((n + 2),(len C)))) + (n + 1) = len C by A42;
then k + (n + 1) <= len C by A47, XREAL_1:6;
hence nk <= len C ; :: thesis:

end;

then n = 1 by A49, A5, GLIB_001:def 28;
hence contradiction by A16; :: thesis:

end;

then reconsider P1 = C .cut (1,m), P2 = C .cut ((n + 2),(len C)) as Walk of G2 by A1, Th64;
set w1 = C . m;
set w2 = C . (n + 2);
set e1 = C . (m + 1);
set e2 = C . (n + 1);
n - 2 < (len C) - 0 by A14, XREAL_1:15;
then ( C . (m + 1) Joins C . m,C . (m + 2),G1 & C . (n + 1) Joins C . n,C . (n + 2),G1 ) by GLIB_001:def 3, A16;
then A50: ( C . (m + 1) Joins C . m,v,G1 & C . (n + 1) Joins C . (n + 2),v,G1 ) by A38, GLIB_000:14, A15;
then A51: ( C . m in V & C . (n + 2) in V ) by A1, Def4;
then reconsider w1 = C . m, w2 = C . (n + 2) as Vertex of G2 by A1;
( (C .cut (1,m)) .first() = C . 1 & (C .cut (1,m)) .last() = C . m ) by A39, Lm16, GLIB_001:37;
then A52: ( (C .cut (1,m)) .first() = v1 & (C .cut (1,m)) .last() = w1 ) by GLIB_001:def 6;
( (C .cut ((n + 2),(len C))) .first() = w2 & (C .cut ((n + 2),(len C))) .last() = C . (len C) ) by A40, GLIB_001:37;
then ( (C .cut ((n + 2),(len C))) .first() = w2 & (C .cut ((n + 2),(len C))) .last() = v1 ) by A7, GLIB_001:def 7;
then A53: ( ((C .cut ((n + 2),(len C))) .reverse()) .first() = v1 & ((C .cut ((n + 2),(len C))) .reverse()) .last() = w2 ) by GLIB_001:22;
w1 in G2 .reachableFrom v1 by A1, A43, A52, Th69;
then reconsider w1 = w1 as Vertex of the inducedSubgraph of G2,(G2 .reachableFrom v1) by GLIB_000:def 37;
w2 in G2 .reachableFrom v1

proof

assume not w2 in G2 .reachableFrom v1 ; :: thesis:
then v in ((C .cut ((n + 2),(len C))) .reverse()) .vertices() by A1, A53, Th69;
then v in (C .cut ((n + 2),(len C))) .vertices() by GLIB_001:92;
hence contradiction by A43; :: thesis:

end;

then reconsider w2 = w2 as Vertex of the inducedSubgraph of G2,(G2 .reachableFrom v1) by GLIB_000:def 37;
A54: w1 = w2 by A51, A3;
consider e3 being object such that
( e3 in E & e3 Joins w1,v,G1 ) and
A55: for e5 being object st e5 Joins w1,v,G1 holds
e5 = e3 by A4, A51;
( C . (m + 1) = e3 & C . (n + 1) = e3 ) by A54, A50, A55;
then A56: C . (n - 1) = C . (n + 1) ;
reconsider n2 = m + 1 as even Element of NAT ;
n + (- 1) < n + 1 by XREAL_1:8;
then A57: n2 < n + 1 ;
A58: 1 + 0 <= m + 1 by XREAL_1:7;
(n + 2) - 1 <= (len C) - 0 by A40, XREAL_1:13;
then ( 1 <= n2 & n2 < n + 1 & n + 1 <= len C ) by A57, A58;
then C . n2 <> C . (n + 1) by A6, GLIB_001:138;
hence contradiction by A56; :: thesis:

end;

suppose A59: C .first() = v ; :: thesis:

A60: len C >= 5

proof

assume len C < 5 ; :: thesis:
then len C < 4 + 1 ;
then len C <= 4 by NAT_1:13;
then A61: len C = 3 by A5, GLIB_001:126, CHORD:7;
then 1 < len C ;
then C . (1 + 1) Joins C . 1,C . (1 + 2),G1 by Lm16, GLIB_001:def 3;
then C . 2 Joins C .first() ,C . (len C),G1 by A61, GLIB_001:def 6;
then C . 2 Joins C .first() ,C .last() ,G1 by GLIB_001:def 7;
then C . 2 Joins v,v,G1 by A59, A7;
hence contradiction by A1, Def4; :: thesis:

end;

A62: 1 < len C

proof

assume A63: 1 >= len C ; :: thesis:
1 <= len C by ABIAN:12;
then len C = 1 by A63, XXREAL_0:1;
hence contradiction by A60; :: thesis:

end;

then reconsider m = (len C) - 2 as odd Element of NAT by Lm13;
(len C) - 2 < (len C) - 0 by XREAL_1:15;
then A64: m < len C ;
set w1 = C . 3;
set w2 = C . m;
set e1 = C . 2;
set e2 = C . (m + 1);
set P = C .cut (3,m);
A65: 3 is odd Element of NAT by Lm16;
A66: (len C) - 2 <= (len C) - 0 by XREAL_1:13;
5 - 2 <= (len C) - 2 by A60, XREAL_1:9;
then A67: ( 3 <= m & m <= len C ) by A66;
then (len (C .cut (3,m))) + 3 = ((len C) - 2) + 1 by A65, GLIB_001:36;
then A68: (len (C .cut (3,m))) + 4 = len C ;
not v in (C .cut (3,m)) .vertices()

proof

assume v in (C .cut (3,m)) .vertices() ; :: thesis:
then consider k being odd Element of NAT such that
A69: ( k <= len (C .cut (3,m)) & (C .cut (3,m)) . k = v ) by GLIB_001:87;
reconsider k1 = k -' 1 as Element of NAT ;
A70: k1 + 1 = k by Lm14;
k1 < len (C .cut (3,m)) by A69, Lm14;
then (C .cut (3,m)) . (k1 + 1) = C . (3 + k1) by A67, A65, GLIB_001:36;
then A71: C . (3 + k1) = C . (len C) by A7, A59, A69, A70, GLIB_001:def 7;
reconsider k3 = 3 + k1 as odd Element of NAT by Lm15, Lm16;
(len (C .cut (3,m))) + 2 = (len C) - 2 by A68;
then A72: (len (C .cut (3,m))) + 2 < (len C) - 0 by XREAL_1:15;
k3 = (k1 + 1) + 2 ;
then k3 = k + 2 by Lm14;
then k3 <= (len (C .cut (3,m))) + 2 by A69, XREAL_1:6;
then k3 < len C by A72, XXREAL_0:2;
then A73: k3 = 1 by A71, A6, GLIB_001:def 28;
3 <= k3 by NAT_1:11;
hence contradiction by A73; :: thesis:

end;

then reconsider P = C .cut (3,m) as Walk of G2 by A1, Th64;
( C . (1 + 1) Joins C . 1,C . (1 + 2),G1 & C . (m + 1) Joins C . m,C . (m + 2),G1 ) by A62, A64, Lm16, GLIB_001:def 3;
then ( C . 2 Joins C .first() ,C . 3,G1 & C . (m + 1) Joins C . m,C . (len C),G1 ) by GLIB_001:def 6;
then ( C . 2 Joins C . 3,v,G1 & C . (m + 1) Joins C . m,C .last() ,G1 ) by A59, GLIB_000:14, GLIB_001:def 7;
then A74: ( C . 2 Joins C . 3,v,G1 & C . (m + 1) Joins C . m,v,G1 ) by A59, A7;
then A75: ( C . 3 in V & C . m in V ) by A1, Def4;
then reconsider w1 = C . 3, w2 = C . m as Vertex of G2 by A1;
set G3 = the inducedSubgraph of G2,(G2 .reachableFrom w1);
C .cut (3,m) is_Walk_from w1,w2 by A67, Lm16, GLIB_001:37;
then P is_Walk_from w1,w2 by GLIB_001:19;
then w2 in G2 .reachableFrom w1 by GLIB_002:def 5;
then reconsider w2 = w2 as Vertex of the inducedSubgraph of G2,(G2 .reachableFrom w1) by GLIB_000:def 37;
w1 in G2 .reachableFrom w1 by GLIB_002:9;
then reconsider w1 = w1 as Vertex of the inducedSubgraph of G2,(G2 .reachableFrom w1) by GLIB_000:def 37;
A76: w1 = w2 by A3, A75;
consider e3 being object such that
( e3 in E & e3 Joins w1,v,G1 ) and
A77: for e5 being object st e5 Joins w1,v,G1 holds
e3 = e5 by A4, A75;
A78: ( C . 2 = e3 & C . (m + 1) = e3 ) by A74, A76, A77;
reconsider n2 = 1 + 1 as even Element of NAT by Lm16;
(len C) - 1 <= (len C) - 0 by XREAL_1:13;
then A79: m + 1 <= len C ;
( 2 < 3 & 3 + 0 <= m + 1 ) by A67, XREAL_1:7;
then ( 1 <= n2 & n2 < m + 1 & m + 1 <= len C ) by A79, XXREAL_0:2;
then C . n2 <> C . (m + 1) by A5, GLIB_001:138;
hence contradiction by A78; :: thesis:

end;

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