let G be Cycle-like _Graph; :: thesis:
let C be Circuit-like Walk of G; :: thesis:

now :: thesis:

given x being object such that A1: ( x in the_Vertices_of G & not x in C .vertices() ) ; :: thesis:
reconsider x = x as Vertex of G by A1;
consider W being Walk of G such that
A2: W is_Walk_from C .first() ,x by GLIB_002:def 1;
defpred S₁[ Nat] means ( $1 is odd & $1 <= len W & not W . $1 in C .vertices() );
A3: ex k being Nat st S₁[k]

proof

take k = len W; :: thesis:
thus k is odd ; :: thesis:
W .last() = x by A2, GLIB_001:def 23;
hence ( k <= len W & not W . k in C .vertices() ) by A1; :: thesis:

end;

consider k being Nat such that
A4: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A3);
2 < k

proof

assume k <= 2 ; :: thesis:
then not W .first() in C .vertices() by A4, CHORD:6;
then not C .first() in C .vertices() by A2, GLIB_001:def 23;
hence contradiction by GLIB_001:88; :: thesis:

end;

then reconsider k2 = k - 2 as odd Element of NAT by A4, INT_1:5, POLYFORM:5;
A5: ( k2 <= k - 0 & k2 < k - 0 ) by XREAL_1:10;
then k2 <= len W by A4, XXREAL_0:2;
then A7: W . k2 in C .vertices() by A4, A5;
then consider m being odd Element of NAT such that
A8: ( m <= len C & C . m = W . k2 ) by GLIB_001:87;
reconsider w = W . k2 as Vertex of G by A7;
k2 < len W by A4, A5, XXREAL_0:2;
then A9: W . (k2 + 1) Joins W . k2,W . (k2 + 2),G by GLIB_001:def 3;
3 c= w .degree()

proof

A10: len C >= 3 by GLIB_001:125;
then reconsider n = (len C) - 2 as odd Element of NAT by INT_1:5, POLYFORM:5, XXREAL_0:2;
n < (len C) - 0 by XREAL_1:10;
then A11: C . (n + 1) Joins C . n,C . (n + 2),G by GLIB_001:def 3;

per cases ;

suppose A12: m = 1 ; :: thesis:

then m < len C by A10, XXREAL_0:2;
then A13: C . (m + 1) Joins C . m,C . (m + 2),G by GLIB_001:def 3;
3 - 2 <= n by A10, XREAL_1:9;

per cases by A12, XXREAL_0:1;

suppose n > m ; :: thesis:

then A14: n + 1 > m + 1 by XREAL_1:6;
A15: 1 + 0 <= 1 + m by XREAL_1:6;
n + 1 <= ((len C) - 2) + 2 by XREAL_1:6;
then A17: C . (m + 1) <> C . (n + 1) by A14, A15, GLIB_001:138;
set M = {(C . (m + 1)),(W . (k2 + 1)),(C . (n + 1))};
( W . (k2 + 1) <> C . (m + 1) & W . (k2 + 1) <> C . (n + 1) )

proof

assume ( W . (k2 + 1) = C . (m + 1) or W . (k2 + 1) = C . (n + 1) ) ; :: thesis:

per cases ;

suppose W . (k2 + 1) = C . (m + 1) ; :: thesis:

then A18: ( W . k = C . m or W . k = C . (m + 2) ) by A9, A13, GLIB_000:15;
( m <= len C & m + 2 <= len C ) by A10, A12, XXREAL_0:2;
hence contradiction by A4, A18, GLIB_001:87; :: thesis:

end;

suppose W . (k2 + 1) = C . (n + 1) ; :: thesis:

then A19: ( W . k = C . n or W . k = C . (n + 2) ) by A9, A11, GLIB_000:15;
n + 0 <= n + 2 by XREAL_1:6;
hence contradiction by A4, A19, GLIB_001:87; :: thesis:

end;

then A20: card {(C . (m + 1)),(W . (k2 + 1)),(C . (n + 1))} = 3 by A17, CARD_2:58;

now :: thesis:

let x be object ; :: thesis:
assume x in {(C . (m + 1)),(W . (k2 + 1)),(C . (n + 1))} ; :: thesis:

per cases by ENUMSET1:def 1;

suppose x = C . (m + 1) ; :: thesis:

hence x in w .edgesInOut() by A8, A13, GLIB_000:62; :: thesis:

end;

suppose x = W . (k2 + 1) ; :: thesis:

hence x in w .edgesInOut() by A9, GLIB_000:62; :: thesis:

end;

suppose x = C . (n + 1) ; :: thesis:

then x Joins C .last() ,C . n,G by A11, GLIB_000:14;
then x Joins C .first() ,C . n,G by GLIB_001:def 24;
hence x in w .edgesInOut() by A8, A12, GLIB_000:62; :: thesis:

end;

then A21: 3 c= card (w .edgesInOut()) by A20, CARD_1:11, TARSKI:def 3;
card (w .edgesInOut()) c= w .degree() by CARD_2:34;
hence 3 c= w .degree() by A21, XBOOLE_1:1; :: thesis:

end;

suppose n = m ; :: thesis:

then C . 3 = w by A8, A12, GLIB_001:118;
then A23: C . 2 Joins w,w,G by A8, A12, A13;
A24: C . 2 <> W . (k2 + 1) by A4, A7, A9, A23, GLIB_000:15;
A25: ( C . 2 in w .edgesIn() & C . 2 in w .edgesOut() ) by A23, GLIB_000:63;

per cases by A9, GLIB_000:16;

suppose W . (k2 + 1) DJoins w,W . (k2 + 2),G ; :: thesis:

then W . (k2 + 1) in w .edgesOut() by GLIB_000:59;
then card {(C . 2),(W . (k2 + 1))} c= w .outDegree() by A25, ZFMISC_1:32, CARD_1:11;
then A26: 2 c= w .outDegree() by A24, CARD_2:57;
card {(C . 2)} c= w .inDegree() by A25, ZFMISC_1:31, CARD_1:11;
then 1 c= w .inDegree() by CARD_1:30;
then 2 +` 1 c= w .degree() by A26, CARD_2:83;
hence 3 c= w .degree() ; :: thesis:

end;

suppose W . (k2 + 1) DJoins W . (k2 + 2),w,G ; :: thesis:

then W . (k2 + 1) in w .edgesIn() by GLIB_000:57;
then card {(C . 2),(W . (k2 + 1))} c= w .inDegree() by A25, ZFMISC_1:32, CARD_1:11;
then A27: 2 c= w .inDegree() by A24, CARD_2:57;
card {(C . 2)} c= w .outDegree() by A25, ZFMISC_1:31, CARD_1:11;
then 1 c= w .outDegree() by CARD_1:30;
then 1 +` 2 c= w .degree() by A27, CARD_2:83;
hence 3 c= w .degree() ; :: thesis:

end;

suppose A28: m = len C ; :: thesis:

reconsider l = 1 as odd Element of NAT by POLYFORM:4;
l < len C by A10, XXREAL_0:2;
then A29: C . (l + 1) Joins C . l,C . (l + 2),G by GLIB_001:def 3;
3 - 2 <= n by A10, XREAL_1:9;

per cases by XXREAL_0:1;

suppose n > 1 ; :: thesis:

then A30: ( n + 1 > l + 1 & 1 + 0 <= 1 + k ) by XREAL_1:6;
n + 1 <= ((len C) - 2) + 2 by XREAL_1:6;
then A31: C . (l + 1) <> C . (n + 1) by A30, GLIB_001:138;
set M = {(C . (l + 1)),(W . (k2 + 1)),(C . (n + 1))};
( W . (k2 + 1) <> C . (l + 1) & W . (k2 + 1) <> C . (n + 1) )

proof

assume ( W . (k2 + 1) = C . (l + 1) or W . (k2 + 1) = C . (n + 1) ) ; :: thesis:

per cases ;

suppose W . (k2 + 1) = C . (l + 1) ; :: thesis:

then A32: ( W . k = C . l or W . k = C . (l + 2) ) by A9, A29, GLIB_000:15;
( l <= len C & l + 2 <= len C ) by A10, XXREAL_0:2;
hence contradiction by A4, A32, GLIB_001:87; :: thesis:

end;

suppose W . (k2 + 1) = C . (n + 1) ; :: thesis:

then A33: ( W . k = C . n or W . k = C . (n + 2) ) by A9, A11, GLIB_000:15;
n + 0 <= n + 2 by XREAL_1:6;
hence contradiction by A4, A33, GLIB_001:87; :: thesis:

end;

then A34: card {(C . (l + 1)),(W . (k2 + 1)),(C . (n + 1))} = 3 by A31, CARD_2:58;

now :: thesis:

let x be object ; :: thesis:
assume x in {(C . (l + 1)),(W . (k2 + 1)),(C . (n + 1))} ; :: thesis:

per cases by ENUMSET1:def 1;

suppose x = C . (l + 1) ; :: thesis:

then x Joins C .first() ,C . (l + 2),G by A29;
then x Joins C .last() ,C . (l + 2),G by GLIB_001:def 24;
hence x in w .edgesInOut() by A8, A28, GLIB_000:62; :: thesis:

end;

suppose x = W . (k2 + 1) ; :: thesis:

hence x in w .edgesInOut() by A9, GLIB_000:62; :: thesis:

end;

suppose x = C . (n + 1) ; :: thesis:

hence x in w .edgesInOut() by A8, A11, A28, GLIB_000:14, GLIB_000:62; :: thesis:

end;

then A35: 3 c= card (w .edgesInOut()) by A34, CARD_1:11, TARSKI:def 3;
card (w .edgesInOut()) c= w .degree() by CARD_2:34;
hence 3 c= w .degree() by A35, XBOOLE_1:1; :: thesis:

end;

suppose n = 1 ; :: thesis:

then A37: len C = 3 ;
then A38: C . 3 = w by A8, A28;
then w = C .last() by A37;
then w = C .first() by GLIB_001:def 24;
then A39: C . 2 Joins w,w,G by A29, A38;
A40: C . 2 <> W . (k2 + 1) by A4, A7, A9, A39, GLIB_000:15;
A41: ( C . 2 in w .edgesIn() & C . 2 in w .edgesOut() ) by A39, GLIB_000:63;

per cases by A9, GLIB_000:16;

suppose W . (k2 + 1) DJoins w,W . (k2 + 2),G ; :: thesis:

then W . (k2 + 1) in w .edgesOut() by GLIB_000:59;
then card {(C . 2),(W . (k2 + 1))} c= w .outDegree() by A41, ZFMISC_1:32, CARD_1:11;
then A42: 2 c= w .outDegree() by A40, CARD_2:57;
card {(C . 2)} c= w .inDegree() by A41, ZFMISC_1:31, CARD_1:11;
then 1 c= w .inDegree() by CARD_1:30;
then 2 +` 1 c= w .degree() by A42, CARD_2:83;
hence 3 c= w .degree() ; :: thesis:

end;

suppose W . (k2 + 1) DJoins W . (k2 + 2),w,G ; :: thesis:

then W . (k2 + 1) in w .edgesIn() by GLIB_000:57;
then card {(C . 2),(W . (k2 + 1))} c= w .inDegree() by A41, ZFMISC_1:32, CARD_1:11;
then A43: 2 c= w .inDegree() by A40, CARD_2:57;
card {(C . 2)} c= w .outDegree() by A41, ZFMISC_1:31, CARD_1:11;
then 1 c= w .outDegree() by CARD_1:30;
then 1 +` 2 c= w .degree() by A43, CARD_2:83;
hence 3 c= w .degree() ; :: thesis:

end;

suppose A44: ( m <> 1 & m <> len C ) ; :: thesis:

then A45: m < len C by A8, XXREAL_0:1;
then A46: C . (m + 1) Joins C . m,C . (m + 2),G by GLIB_001:def 3;
0 < m ;
then 0 + 1 <= m by INT_1:7;
then m > 1 by A44, XXREAL_0:1;
then m >= 1 + 1 by INT_1:7;
then reconsider l = m - 2 as odd Element of NAT by INT_1:5, POLYFORM:5;
A48: l < m - 0 by XREAL_1:10;
then A49: l < len C by A45, XXREAL_0:2;
then A50: C . (l + 1) Joins C . l,C . (l + 2),G by GLIB_001:def 3;
A51: m + 1 > l + 1 by A48, XREAL_1:6;
A52: 1 + 0 <= l + 1 by XREAL_1:6;
m + 1 <= len C by A45, INT_1:7;
then A53: C . (m + 1) <> C . (l + 1) by A51, A52, GLIB_001:138;
set M = {(C . (m + 1)),(W . (k2 + 1)),(C . (l + 1))};
( W . (k2 + 1) <> C . (m + 1) & W . (k2 + 1) <> C . (l + 1) )

proof

assume ( W . (k2 + 1) = C . (m + 1) or W . (k2 + 1) = C . (l + 1) ) ; :: thesis:

per cases ;

suppose W . (k2 + 1) = C . (m + 1) ; :: thesis:

then A54: ( W . k = C . m or W . k = C . (m + 2) ) by A9, A46, GLIB_000:15;
( m <= len C & m + 2 <= len C ) by A45, CHORD:4;
hence contradiction by A4, A54, GLIB_001:87; :: thesis:

end;

suppose W . (k2 + 1) = C . (l + 1) ; :: thesis:

then ( W . k = C . l or W . k = C . (l + 2) ) by A9, A50, GLIB_000:15;
hence contradiction by A4, A45, A49, GLIB_001:87; :: thesis:

end;

then A56: card {(C . (m + 1)),(W . (k2 + 1)),(C . (l + 1))} = 3 by A53, CARD_2:58;

now :: thesis:

let x be object ; :: thesis:
assume x in {(C . (m + 1)),(W . (k2 + 1)),(C . (l + 1))} ; :: thesis:

per cases by ENUMSET1:def 1;

suppose x = C . (m + 1) ; :: thesis:

hence x in w .edgesInOut() by A8, A46, GLIB_000:62; :: thesis:

end;

suppose x = W . (k2 + 1) ; :: thesis:

hence x in w .edgesInOut() by A9, GLIB_000:62; :: thesis:

end;

suppose x = C . (l + 1) ; :: thesis:

hence x in w .edgesInOut() by A8, A50, GLIB_000:14, GLIB_000:62; :: thesis:

end;

then A57: 3 c= card (w .edgesInOut()) by A56, CARD_1:11, TARSKI:def 3;
card (w .edgesInOut()) c= w .degree() by CARD_2:34;
hence 3 c= w .degree() by A57, XBOOLE_1:1; :: thesis:

end;

then Segm 3 c= Segm 2 by GLIB_016:def 4;
hence contradiction by NAT_1:39; :: thesis:

end;

then the_Vertices_of G c= C .vertices() by TARSKI:def 3;
hence A58: C .vertices() = the_Vertices_of G by XBOOLE_0:def 10; :: thesis:

now :: thesis:

given x being object such that A59: ( x in the_Edges_of G & not x in C .edges() ) ; :: thesis:
set w = (the_Source_of G) . x;
reconsider w = (the_Source_of G) . x as Vertex of G by A59, FUNCT_2:5;
consider m being odd Element of NAT such that
A60: ( m <= len C & C . m = w ) by A58, GLIB_001:87;
3 c= w .degree()

proof

A61: len C >= 3 by GLIB_001:125;
then reconsider n = (len C) - 2 as odd Element of NAT by INT_1:5, POLYFORM:5, XXREAL_0:2;
A62: n < (len C) - 0 by XREAL_1:10;
then A63: C . (n + 1) Joins C . n,C . (n + 2),G by GLIB_001:def 3;

per cases ;

suppose A64: m = 1 ; :: thesis:

m < len C by A61, A64, XXREAL_0:2;
then A65: C . (m + 1) Joins C . m,C . (m + 2),G by GLIB_001:def 3;
3 - 2 <= n by A61, XREAL_1:9;

per cases by A64, XXREAL_0:1;

suppose A66: n > m ; :: thesis:

then A67: n + 1 > m + 1 by XREAL_1:6;
A68: 1 + 0 <= 1 + m by XREAL_1:6;
n + 1 <= ((len C) - 2) + 2 by XREAL_1:6;
then A70: C . (m + 1) <> C . (n + 1) by A67, A68, GLIB_001:138;
set M = {(C . (m + 1)),x,(C . (n + 1))};
( x <> C . (m + 1) & x <> C . (n + 1) )

proof

m < len C by A62, A66, XXREAL_0:2;
hence ( x <> C . (m + 1) & x <> C . (n + 1) ) by A59, A62, GLIB_001:100; :: thesis:

end;

then A71: card {(C . (m + 1)),x,(C . (n + 1))} = 3 by A70, CARD_2:58;

now :: thesis:

let y be object ; :: thesis:
assume y in {(C . (m + 1)),x,(C . (n + 1))} ; :: thesis:

per cases by ENUMSET1:def 1;

suppose y = C . (m + 1) ; :: thesis:

hence y in w .edgesInOut() by A60, A65, GLIB_000:62; :: thesis:

end;

suppose y = x ; :: thesis:

hence y in w .edgesInOut() by A59, GLIB_000:61; :: thesis:

end;

suppose y = C . (n + 1) ; :: thesis:

then y Joins C .last() ,C . n,G by A63, GLIB_000:14;
then y Joins C .first() ,C . n,G by GLIB_001:def 24;
hence y in w .edgesInOut() by A60, A64, GLIB_000:62; :: thesis:

end;

then A72: 3 c= card (w .edgesInOut()) by A71, CARD_1:11, TARSKI:def 3;
card (w .edgesInOut()) c= w .degree() by CARD_2:34;
hence 3 c= w .degree() by A72, XBOOLE_1:1; :: thesis:

end;

suppose n = m ; :: thesis:

then A74: len C = 3 by A64;
then A75: C . 2 Joins w,w,G by A60, A64, A65, GLIB_001:118;
A76: C . 2 <> x

proof

C . (1 + 1) in C .edges() by A74, POLYFORM:4, GLIB_001:100;
hence C . 2 <> x by A59; :: thesis:

end;

A77: ( C . 2 in w .edgesIn() & C . 2 in w .edgesOut() ) by A75, GLIB_000:63;
x in w .edgesOut() by A59, GLIB_000:58;
then card {(C . 2),x} c= w .outDegree() by A77, ZFMISC_1:32, CARD_1:11;
then A78: 2 c= w .outDegree() by A76, CARD_2:57;
card {(C . 2)} c= w .inDegree() by CARD_1:11, A77, ZFMISC_1:31;
then 1 c= w .inDegree() by CARD_1:30;
then 2 +` 1 c= w .degree() by A78, CARD_2:83;
hence 3 c= w .degree() ; :: thesis:

end;

suppose A79: m = len C ; :: thesis:

reconsider l = 1 as odd Element of NAT by POLYFORM:4;
A80: l < len C by A61, XXREAL_0:2;
then A81: C . (l + 1) Joins C . l,C . (l + 2),G by GLIB_001:def 3;
3 - 2 <= n by A61, XREAL_1:9;

per cases by XXREAL_0:1;

suppose n > 1 ; :: thesis:

then A82: ( n + 1 > l + 1 & 1 + 0 <= 1 + l ) by XREAL_1:6;
n + 1 <= ((len C) - 2) + 2 by XREAL_1:6;
then A83: C . (l + 1) <> C . (n + 1) by A82, GLIB_001:138;
set M = {(C . (l + 1)),x,(C . (n + 1))};
( x <> C . (l + 1) & x <> C . (n + 1) ) by A59, A62, A80, GLIB_001:100;
then A84: card {(C . (l + 1)),x,(C . (n + 1))} = 3 by A83, CARD_2:58;

now :: thesis:

let y be object ; :: thesis:
assume y in {(C . (l + 1)),x,(C . (n + 1))} ; :: thesis:

per cases by ENUMSET1:def 1;

suppose y = C . (l + 1) ; :: thesis:

then y Joins C .first() ,C . (l + 2),G by A81;
then y Joins C .last() ,C . (l + 2),G by GLIB_001:def 24;
hence y in w .edgesInOut() by A60, A79, GLIB_000:62; :: thesis:

end;

suppose y = x ; :: thesis:

hence y in w .edgesInOut() by A59, GLIB_000:61; :: thesis:

end;

suppose y = C . (n + 1) ; :: thesis:

hence y in w .edgesInOut() by A60, A63, A79, GLIB_000:14, GLIB_000:62; :: thesis:

end;

then A85: 3 c= card (w .edgesInOut()) by A84, CARD_1:11, TARSKI:def 3;
card (w .edgesInOut()) c= w .degree() by CARD_2:34;
hence 3 c= w .degree() by A85, XBOOLE_1:1; :: thesis:

end;

suppose n = 1 ; :: thesis:

then A87: len C = 3 ;
then A88: C . 3 = w by A60, A79;
then w = C .last() by A87;
then w = C .first() by GLIB_001:def 24;
then A89: C . 2 Joins w,w,G by A81, A88;
A90: C . 2 <> x

proof

C . (1 + 1) in C .edges() by A87, POLYFORM:4, GLIB_001:100;
hence C . 2 <> x by A59; :: thesis:

end;

A91: ( C . 2 in w .edgesIn() & C . 2 in w .edgesOut() ) by A89, GLIB_000:63;
x in w .edgesOut() by A59, GLIB_000:58;
then card {(C . 2),x} c= w .outDegree() by A91, ZFMISC_1:32, CARD_1:11;
then A92: 2 c= w .outDegree() by A90, CARD_2:57;
card {(C . 2)} c= w .inDegree() by A91, ZFMISC_1:31, CARD_1:11;
then 1 c= w .inDegree() by CARD_1:30;
then 2 +` 1 c= w .degree() by A92, CARD_2:83;
hence 3 c= w .degree() ; :: thesis:

end;

suppose A93: ( m <> 1 & m <> len C ) ; :: thesis:

then A94: m < len C by A60, XXREAL_0:1;
then A95: C . (m + 1) Joins C . m,C . (m + 2),G by GLIB_001:def 3;
0 < m ;
then 0 + 1 <= m by INT_1:7;
then m > 1 by A93, XXREAL_0:1;
then m >= 1 + 1 by INT_1:7;
then reconsider l = m - 2 as odd Element of NAT by INT_1:5, POLYFORM:5;
A97: l < m - 0 by XREAL_1:10;
then A98: l < len C by A94, XXREAL_0:2;
then A99: C . (l + 1) Joins C . l,C . (l + 2),G by GLIB_001:def 3;
A100: m + 1 > l + 1 by A97, XREAL_1:6;
A101: 1 + 0 <= l + 1 by XREAL_1:6;
m + 1 <= len C by A94, INT_1:7;
then A102: C . (m + 1) <> C . (l + 1) by A100, A101, GLIB_001:138;
set M = {(C . (m + 1)),x,(C . (l + 1))};
( x <> C . (m + 1) & x <> C . (l + 1) ) by A59, A94, A98, GLIB_001:100;
then A103: card {(C . (m + 1)),x,(C . (l + 1))} = 3 by A102, CARD_2:58;

now :: thesis:

let y be object ; :: thesis:
assume y in {(C . (m + 1)),x,(C . (l + 1))} ; :: thesis:

per cases by ENUMSET1:def 1;

suppose y = C . (m + 1) ; :: thesis:

hence y in w .edgesInOut() by A60, A95, GLIB_000:62; :: thesis:

end;

suppose y = x ; :: thesis:

hence y in w .edgesInOut() by A59, GLIB_000:61; :: thesis:

end;

suppose y = C . (l + 1) ; :: thesis:

hence y in w .edgesInOut() by A60, A99, GLIB_000:14, GLIB_000:62; :: thesis:

end;

then A104: 3 c= card (w .edgesInOut()) by A103, CARD_1:11, TARSKI:def 3;
card (w .edgesInOut()) c= w .degree() by CARD_2:34;
hence 3 c= w .degree() by A104, XBOOLE_1:1; :: thesis:

end;

then Segm 3 c= Segm 2 by GLIB_016:def 4;
hence contradiction by NAT_1:39; :: thesis:

end;

then the_Edges_of G c= C .edges() by TARSKI:def 3;
hence C .edges() = the_Edges_of G by XBOOLE_0:def 10; :: thesis: