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

per cases ;

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

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

A9: now :: thesis:

per cases by A7;

suppose n = 1 ; :: thesis:

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

end;

suppose n = len C ; :: thesis:

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

end;

then A10: x <> Ci by A8, GLIB_001:def 28;
(len C) + (- 2) >= 9 + (- 2) by A3, XREAL_1:7;
then (len C) - (2 * 1) >= 0 by XXREAL_0:2;
then (len C) - 2 is odd Element of NAT by INT_1:3;
then reconsider j = (len C) - 2 as odd Nat ;
take i ; :: thesis:
take j ; :: thesis:
A11: (len C) + (- 2) >= 9 + (- 2) by A3, XREAL_1:7;
hence i + 2 < j by XXREAL_0:2; :: thesis:
A12: (len C) + 0 > (len C) + (- 2) by XREAL_1:8;
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 A13: C . i = C . j ; :: thesis:
(i + 2) + (- 2) < j + 0 by A11, XXREAL_0:2;
hence contradiction by A12, A13, GLIB_001:def 28; :: thesis:

end;

(len C) + 0 > 9 + (- 8) by A3, XREAL_1:8;
then C . (k + 1) Joins C . k,C . i,G by GLIB_001:def 3;
then x,Ci are_adjacent by A9;
hence C . i in G .AdjacentSet {x} by A10, Th51; :: thesis:
A14: j in NAT by ORDINAL1:def 12;
then reconsider Cj = C . j as Vertex of G by A12, GLIB_001:7;

A15: now :: thesis:

per cases by A7;

suppose n = 1 ; :: thesis:

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

end;

suppose n = len C ; :: thesis:

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

end;

A16: now :: thesis:

assume x = Cj ; :: thesis:
then A17: j = 1 by A14, A12, A15, GLIB_001:def 28;
j + 2 = len C ;
hence contradiction by A3, A17; :: thesis:

end;

C . (j + 1) Joins Cj,x,G by A14, A12, A15, GLIB_001:def 3;
then x,Cj are_adjacent by Def3;
hence C . j in G .AdjacentSet {x} by A16, Th51; :: thesis:

end;

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

then (2 * 0) + 1 < n by A6, XXREAL_0:1;
then 1 + 2 <= n by Th4;
then 3 + (- 2) <= n + (- 2) by XREAL_1:7;
then 0 <= n - (2 * 1) ;
then n - 2 is odd Element of NAT by INT_1:3;
then reconsider i = n - 2 as odd Nat ;
A19: i + 0 < i + 2 by XREAL_1:8;
then reconsider Ci = C . i as Vertex of G by A4, GLIB_001:7, XXREAL_0:2;
reconsider j = n + 2 as odd Nat ;
A20: n < len C by A4, A18, XXREAL_0:1;
then A21: n + 2 <= ((len C) - 2) + 2 by Th4;
then reconsider Cj = C . j as Vertex of G by GLIB_001:7;

A22: now :: thesis:

A23: n + 2 > n + 0 by XREAL_1:8;
assume Cj = x ; :: thesis:
hence contradiction by A5, A18, A21, A23, GLIB_001:def 28; :: thesis:

end;

take i ; :: thesis:
take j ; :: thesis:
n + 0 < n + 2 by XREAL_1:8;
hence ( i + 2 < j & j <= len C ) by A20, Th4; :: thesis:

A24: now :: thesis:

assume that
A25: i = 1 and
A26: j = len C ; :: thesis:
j = i + 4 ;
hence contradiction by A3, A25, A26; :: thesis:

end;

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

hereby :: thesis:

assume that
A27: i = 1 and
A28: j = (len C) - 2 ; :: thesis:
(len C) + (- 2) >= 9 + (- 3) by A3, XREAL_1:7;
hence contradiction by A27, A28; :: thesis:

end;

hereby :: thesis:

assume that
A29: i = 3 and
A30: j = len C ; :: thesis:
j = i + 4 ;
hence contradiction by A3, A29, A30; :: thesis:

end;

A31: i in NAT by ORDINAL1:def 12;

A32: now :: thesis:

A33: n + 0 > n + (- 2) by XREAL_1:8;
assume Ci = x ; :: thesis:
hence contradiction by A4, A5, A18, A31, A33, GLIB_001:def 28; :: thesis:

end;

A34: n + 2 <= ((len C) - 2) + 2 by A20, Th4;

hereby :: thesis:

A35: (i + 2) + (- 2) < j + 0 by XREAL_1:8;
assume C . i = C . j ; :: thesis:
hence contradiction by A31, A34, A24, A35, GLIB_001:def 28; :: thesis:

end;

i < len C by A4, A19, XXREAL_0:2;
then C . (i + 1) Joins C . i,C . (i + 2),G by A31, GLIB_001:def 3;
then x,Ci are_adjacent by A5, Def3;
hence C . i in G .AdjacentSet {x} by A32, Th51; :: thesis:
C . (n + 1) Joins C . n,C . j,G by A20, GLIB_001:def 3;
then x,Cj are_adjacent by A5;
hence C . j in G .AdjacentSet {x} by A22, Th51; :: thesis:

end;