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:
thus ( ( not i = 1 or not j = len C ) & ( not i = 1 or not j = (len C) - 2 ) & ( not i = 3 or not 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: 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 C . (j + 1) Joins Cj,x,G by A8, A10, GLIB_001:def 3;
then A17: x,Cj are_adjacent by Def3;

now

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

end;

hence C . j in G .AdjacentSet {x} by A17, Th52; :: thesis:

end;

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

then A19: ( (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 0 <= n - (2 * 1) ;
then n - 2 is odd Element of NAT by INT_1:16;
then reconsider i = n - 2 as odd Nat ;
reconsider j = n + 2 as odd Nat ;
take i ; :: thesis:
take j ; :: thesis:
A20: ( i in NAT & j in NAT ) by ORDINAL1:def 13;
A21: ( n + 0 < n + 2 & n + 2 <= ((len C) - 2) + 2 ) by A19, Th4, XREAL_1:10;
hence ( i + 2 < j & j <= len C ) ; :: thesis:

A22: now

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

end;

hence ( not i = 1 or not j = len C ) ; :: thesis:

hereby :: thesis:

assume A24: ( i = 1 & j = (len C) - 2 ) ; :: thesis:
(len C) + (- 2) >= 9 + (- 3) by A3, XREAL_1:9;
hence contradiction by A24; :: thesis:

end;

hereby :: thesis:

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

end;

hereby :: thesis:

assume A26: C . i = C . j ; :: thesis:
(i + 2) + (- 2) < j + 0 by XREAL_1:10;
hence contradiction by A20, A21, A22, A26, GLIB_001:def 28; :: thesis:

end;

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

now

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

end;

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

now

assume A33: Cj = x ; :: thesis:
n + 2 > n + 0 by XREAL_1:10;
hence contradiction by A4, A18, A31, A33, GLIB_001:def 28; :: thesis:

end;

hence C . j in G .AdjacentSet {x} by A32, Th52; :: thesis:

end;