let G be _Graph; :: thesis:
let C be Path of G; :: thesis:
assume A1: ( C is Cycle-like & C .length() > 3 ) ; :: thesis:
let x be Vertex of G; :: thesis:
assume A2: x in C .vertices() ; :: thesis:
C .length() >= 3 + 1 by A1, NAT_1:13;
then 2 * (C .length() ) >= 2 * 4 by XREAL_1:66;
then (2 * (C .length() )) + 1 >= 8 + 1 by XREAL_1:9;
then A3: len C >= 9 by GLIB_001:113;
consider n being odd Element of NAT such that
A4: ( n <= len C & C . n = x ) by A2, GLIB_001:88;
A5: 0 + 1 <= n by HEYTING3:1;
A6: C is closed by A1;

per cases ;

suppose A7: ( n = 1 or n = len C ) ; :: thesis:

reconsider i = (2 * 1) + 1 as odd Nat ;
(len C) + (- 2) >= 9 + (- 2) by A3, XREAL_1:9;
then (len C) - (2 * 1) >= 0 by XXREAL_0:2;
then (len C) - 2 is odd Element of NAT by INT_1:16;
then reconsider j = (len C) - 2 as odd Nat ;
take i ; :: thesis:
take j ; :: thesis:
A8: ( i in NAT & j in NAT ) by ORDINAL1:def 13;
A9: (len C) + (- 2) >= 9 + (- 2) by A3, XREAL_1:9;
hence i + 2 < j by XXREAL_0:2; :: thesis:
A10: (len C) + 0 > (len C) + (- 2) by XREAL_1:10;
hence j <= len C ; :: thesis:

hereby :: thesis:

assume A11: C . i = C . j ; :: thesis:
(i + 2) + (- 2) < j + 0 by A9, XXREAL_0:2;
hence contradiction by A10, A11, GLIB_001:def 28; :: thesis:

end;

reconsider k = (2 * 0 ) + 1 as odd Nat ;
A12: (len C) + 0 > 9 + (- 6) by A3, XREAL_1:10;
then reconsider Ci = C . i as Vertex of G by GLIB_001:8;
(len C) + 0 > 9 + (- 8) by A3, XREAL_1:10;
then A13: C . (k + 1) Joins C . k,C . i,G by GLIB_001:def 3;

A14: now

per cases by A7;

suppose n = 1 ; :: thesis:

hence x = C . k by A4; :: thesis:

end;

suppose n = len C ; :: thesis:

then x = C .last() by A4;
then x = C .first() by A6, GLIB_001:def 24;
hence x = C . k ; :: thesis:

end;

then A15: x,Ci are_adjacent by A13, Def3;
x <> Ci by A12, A14, GLIB_001:def 28;
hence C . i in G .AdjacentSet {x} by A15, Th52; :: thesis:
reconsider Cj = C . j as Vertex of G by A8, A10, GLIB_001:8;
A16: C . (j + 1) Joins C . j,C . (j + 2),G by A8, A10, GLIB_001:def 3;

A17: now

per cases by A7;

suppose n = 1 ; :: thesis:

then x = C .first() by A4;
then x = C .last() by A6, GLIB_001:def 24;
hence x = C . (j + 2) ; :: thesis:

end;

suppose n = len C ; :: thesis:

hence x = C . (j + 2) by A4; :: thesis:

end;

then A18: x,Cj are_adjacent by A16, Def3;

now

assume x = Cj ; :: thesis:
then ( j = 1 & j + 2 = len C ) by A8, A10, A17, GLIB_001:def 28;
hence contradiction by A3; :: thesis:

end;

hence C . j in G .AdjacentSet {x} by A18, Th52; :: thesis:
let e be set ; :: thesis:
assume that
A19: e in C .edges() and
A20: e Joins C . i,C . j,G ; :: thesis:
consider k being even Element of NAT such that
A21: 1 <= k and
A22: k <= len C and
A23: C . k = e by A19, GLIB_001:100;
k in dom C by A21, A22, FINSEQ_3:27;
then consider ku1 being odd Element of NAT such that
A24: ku1 = k - 1 and
A25: k - 1 in dom C and
A26: k + 1 in dom C and
A27: C . k Joins C . ku1,C . (k + 1),G by GLIB_001:10;
A28: ( ( ( (the_Source_of G) . e = C . i & (the_Target_of G) . e = C . j ) or ( (the_Source_of G) . e = C . j & (the_Target_of G) . e = C . i ) ) & ( ( (the_Source_of G) . e = C . ku1 & (the_Target_of G) . e = C . (k + 1) ) or ( (the_Source_of G) . e = C . (k + 1) & (the_Target_of G) . e = C . ku1 ) ) ) by A20, A23, A27, GLIB_000:def 15;
A29: ku1 <= len C by A24, A25, FINSEQ_3:27;
A30: k + 1 <= len C by A26, FINSEQ_3:27;
i < j by A9, XXREAL_0:2;
then A31: i < len C by A10, XXREAL_0:2;
A32: j <> 1 by A9;

per cases by A28;

suppose A33: ( C . i = C . ku1 & C . j = C . (k + 1) ) ; :: thesis:

then i + 2 = (k - 1) + (1 + 1) by A24, A29, A31, Th25
.= j by A10, A30, A32, A33, Th25 ;
hence contradiction by A9; :: thesis:

end;

suppose A34: ( C . i = C . (k + 1) & C . j = C . ku1 ) ; :: thesis:

then i = k + 1 by A30, A31, Th25;
hence contradiction by A10, A24, A29, A32, A34, Th25; :: thesis:

end;

suppose A35: ( not n = 1 & not n = len C ) ; :: thesis:

then A36: ( (2 * 0 ) + 1 < n & n < len C ) by A4, A5, XXREAL_0:1;
then ( 1 + 2 <= n & n <= (len C) - 2 ) by Th3, Th4;
then 3 + (- 2) <= n + (- 2) by XREAL_1:9;
then n - (2 * 1) is odd Element of NAT by INT_1:16;
then reconsider i = n - (2 * 1) as odd Nat ;
reconsider j = n + 2 as odd Nat ;
take i ; :: thesis:
take j ; :: thesis:
A37: ( i in NAT & j in NAT ) by ORDINAL1:def 13;
n + 0 < n + 2 by XREAL_1:10;
hence i + 2 < j ; :: thesis:
thus A38: j <= len C by A36, Th4; :: thesis:

A39: now

assume A40: ( i = 1 & j = len C ) ; :: thesis:
j = i + 4 ;
hence contradiction by A3, A40; :: thesis:

end;

hereby :: thesis:

assume A41: C . i = C . j ; :: thesis:
(i + 2) + (- 2) < j + 0 by XREAL_1:10;
hence contradiction by A37, A38, A39, A41, GLIB_001:def 28; :: thesis:

end;

A42: i + 0 < i + 2 by XREAL_1:10;
then A43: i < len C by A4, XXREAL_0:2;
reconsider Ci = C . i as Vertex of G by A4, A42, GLIB_001:8, XXREAL_0:2;
C . (i + 1) Joins C . i,C . (i + 2),G by A37, A43, GLIB_001:def 3;
then A44: x,Ci are_adjacent by A4, Def3;

now

assume A45: Ci = x ; :: thesis:
n + 0 > n + (- 2) by XREAL_1:10;
hence contradiction by A4, A35, A37, A45, GLIB_001:def 28; :: thesis:

end;

hence C . i in G .AdjacentSet {x} by A44, Th52; :: thesis:
A46: n + 2 <= ((len C) - 2) + 2 by A36, Th4;
reconsider Cj = C . j as Vertex of G by A38, GLIB_001:8;
C . (n + 1) Joins C . n,C . j,G by A36, GLIB_001:def 3;
then A47: x,Cj are_adjacent by A4, Def3;

now

assume A48: Cj = x ; :: thesis:
n + 2 > n + 0 by XREAL_1:10;
hence contradiction by A4, A35, A46, A48, GLIB_001:def 28; :: thesis:

end;

hence C . j in G .AdjacentSet {x} by A47, Th52; :: thesis:
let e be set ; :: thesis:
assume that
A49: e in C .edges() and
A50: e Joins C . i,C . j,G ; :: thesis:
consider k being even Element of NAT such that
A51: 1 <= k and
A52: k <= len C and
A53: C . k = e by A49, GLIB_001:100;
k in dom C by A51, A52, FINSEQ_3:27;
then consider ku1 being odd Element of NAT such that
A54: ku1 = k - 1 and
k - 1 in dom C and
A55: k + 1 in dom C and
A56: C . k Joins C . ku1,C . (k + 1),G by GLIB_001:10;
A57: ( ( ( (the_Source_of G) . e = C . i & (the_Target_of G) . e = C . j ) or ( (the_Source_of G) . e = C . j & (the_Target_of G) . e = C . i ) ) & ( ( (the_Source_of G) . e = C . ku1 & (the_Target_of G) . e = C . (k + 1) ) or ( (the_Source_of G) . e = C . (k + 1) & (the_Target_of G) . e = C . ku1 ) ) ) by A50, A53, A56, GLIB_000:def 15;
A58: k - 1 < len C by A52, XREAL_1:148, XXREAL_0:2;
A59: k + 1 <= len C by A55, FINSEQ_3:27;
1 + 2 <= j by A5, XREAL_1:9;
then A60: j <> 1 ;
1 + 1 <= k + 1 by A51, XREAL_1:9;
then A61: k + 1 <> 1 ;

per cases by A57;

suppose A62: ( C . i = C . ku1 & C . j = C . (k + 1) ) ; :: thesis:

then i + 2 = (k - 1) + (1 + 1) by A43, A54, A58, Th25
.= j by A38, A59, A60, A61, A62, Th25 ;
hence contradiction ; :: thesis:

end;

suppose A63: ( C . i = C . (k + 1) & C . j = C . ku1 ) ; :: thesis:

per cases by A38, A43, A54, A58, A59, A63, Th25;

suppose ( i = k + 1 & j = k - 1 ) ; :: thesis:

hence contradiction ; :: thesis:

end;

suppose A64: ( i = k + 1 & k - 1 = 1 & j = len C ) ; :: thesis:

j = i + 4 ;
hence contradiction by A3, A64; :: thesis:

end;

suppose A65: ( i = 1 & k + 1 = len C & j = k - 1 ) ; :: thesis:

then k + 1 = 7 ;
hence contradiction by A3, A65; :: thesis:

end;

suppose ( i = 1 & k + 1 = len C & k - 1 = 1 & j = len C ) ; :: thesis:

hence contradiction ; :: thesis:

end;