let G be _Graph; :: thesis: for C being Path of G st C is Cycle-like & C .length() > 3 holds
for x being Vertex of G st x in C .vertices() holds
ex m, n being odd Nat st
( m + 2 < n & n <= len C & C . m <> C . n & C . m in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . m,C . n,G ) )

let C be Path of G; :: thesis: ( C is Cycle-like & C .length() > 3 implies for x being Vertex of G st x in C .vertices() holds
ex m, n being odd Nat st
( m + 2 < n & n <= len C & C . m <> C . n & C . m in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . m,C . n,G ) ) )

assume that
A1: C is Cycle-like and
A2: C .length() > 3 ; :: thesis: for x being Vertex of G st x in C .vertices() holds
ex m, n being odd Nat st
( m + 2 < n & n <= len C & C . m <> C . n & C . m in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . m,C . n,G ) )

C .length() >= 3 + 1 by ;
then 2 * () >= 2 * 4 by XREAL_1:64;
then (2 * ()) + 1 >= 8 + 1 by XREAL_1:7;
then A3: len C >= 9 by GLIB_001:112;
let x be Vertex of G; :: thesis: ( x in C .vertices() implies ex m, n being odd Nat st
( m + 2 < n & n <= len C & C . m <> C . n & C . m in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . m,C . n,G ) ) )

assume x in C .vertices() ; :: thesis: ex m, n being odd Nat st
( m + 2 < n & n <= len C & C . m <> C . n & C . m in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . m,C . n,G ) )

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 ( n = 1 or n = len C or ( not n = 1 & not n = len C ) ) ;
suppose A7: ( n = 1 or n = len C ) ; :: thesis: ex m, n being odd Nat st
( m + 2 < n & n <= len C & C . m <> C . n & C . m in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . m,C . n,G ) )

reconsider k = (2 * 0) + 1 as odd Nat ;
A8: now :: thesis: x = C . k
per cases ( n = 1 or n = len C ) by A7;
suppose n = 1 ; :: thesis: x = C . k
hence x = C . k by A5; :: thesis: verum
end;
end;
end;
(len C) + (- 2) >= 9 + (- 2) by ;
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 ;
reconsider i = (2 * 1) + 1 as odd Nat ;
take i ; :: thesis: ex n being odd Nat st
( i + 2 < n & n <= len C & C . i <> C . n & C . i in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . n,G ) )

take j ; :: thesis: ( i + 2 < j & j <= len C & C . i <> C . j & C . i in G .AdjacentSet {x} & C . j in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . j,G ) )

A9: (len C) + (- 2) >= 9 + (- 2) by ;
hence i + 2 < j by XXREAL_0:2; :: thesis: ( j <= len C & C . i <> C . j & C . i in G .AdjacentSet {x} & C . j in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . j,G ) )

A10: (len C) + 0 > (len C) + (- 2) by XREAL_1:8;
hence j <= len C ; :: thesis: ( C . i <> C . j & C . i in G .AdjacentSet {x} & C . j in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . j,G ) )

i < j by ;
then A11: i < len C by ;
hereby :: thesis: ( C . i in G .AdjacentSet {x} & C . j in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . j,G ) )
assume A12: C . i = C . j ; :: thesis: contradiction
(i + 2) + (- 2) < j + 0 by ;
hence contradiction by A10, A12, GLIB_001:def 28; :: thesis: verum
end;
A13: (len C) + 0 > 9 + (- 6) by ;
then reconsider Ci = C . i as Vertex of G by GLIB_001:7;
(len C) + 0 > 9 + (- 8) by ;
then C . (k + 1) Joins C . k,C . i,G by GLIB_001:def 3;
then A14: x,Ci are_adjacent by A8;
x <> Ci by ;
hence C . i in G .AdjacentSet {x} by ; :: thesis: ( C . j in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . j,G ) )

A15: j <> 1 by A9;
A16: j in NAT by ORDINAL1:def 12;
then reconsider Cj = C . j as Vertex of G by ;
A17: now :: thesis: x = C . (j + 2)
per cases ( n = 1 or n = len C ) by A7;
suppose n = 1 ; :: thesis: x = C . (j + 2)
then x = C .first() by A5;
then x = C .last() by ;
hence x = C . (j + 2) ; :: thesis: verum
end;
suppose n = len C ; :: thesis: x = C . (j + 2)
hence x = C . (j + 2) by A5; :: thesis: verum
end;
end;
end;
A18: now :: thesis: not x = Cj
assume x = Cj ; :: thesis: contradiction
then A19: j = 1 by ;
j + 2 = len C ;
hence contradiction by A3, A19; :: thesis: verum
end;
C . (j + 1) Joins C . j,C . (j + 2),G by ;
then x,Cj are_adjacent by ;
hence C . j in G .AdjacentSet {x} by ; :: thesis: for e being object st e in C .edges() holds
not e Joins C . i,C . j,G

let e be object ; :: thesis: ( e in C .edges() implies not e Joins C . i,C . j,G )
assume that
A20: e in C .edges() and
A21: e Joins C . i,C . j,G ; :: thesis: contradiction
consider k being even Element of NAT such that
A22: 1 <= k and
A23: k <= len C and
A24: C . k = e by ;
A25: ( ( (the_Source_of G) . e = C . i & () . e = C . j ) or ( () . e = C . j & () . e = C . i ) ) by A21;
k in dom C by ;
then consider ku1 being odd Element of NAT such that
A26: ku1 = k - 1 and
A27: k - 1 in dom C and
A28: k + 1 in dom C and
A29: C . k Joins C . ku1,C . (k + 1),G by GLIB_001:9;
A30: ku1 <= len C by ;
A31: k + 1 <= len C by ;
per cases ( ( C . i = C . ku1 & C . j = C . (k + 1) ) or ( C . i = C . (k + 1) & C . j = C . ku1 ) ) by ;
suppose A32: ( C . i = C . ku1 & C . j = C . (k + 1) ) ; :: thesis: contradiction
then i + 2 = (k - 1) + (1 + 1) by
.= j by A10, A31, A15, A32, Th25 ;
hence contradiction by A9; :: thesis: verum
end;
suppose A33: ( C . i = C . (k + 1) & C . j = C . ku1 ) ; :: thesis: contradiction
end;
end;
end;
suppose A34: ( not n = 1 & not n = len C ) ; :: thesis: ex m, n being odd Nat st
( m + 2 < n & n <= len C & C . m <> C . n & C . m in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . m,C . n,G ) )

then (2 * 0) + 1 < n by ;
then 1 + 2 <= n by Th4;
then 3 + (- 2) <= n + (- 2) by XREAL_1:7;
then n - (2 * 1) is odd Element of NAT by INT_1:3;
then reconsider i = n - (2 * 1) as odd Nat ;
A35: i + 0 < i + 2 by XREAL_1:8;
then reconsider Ci = C . i as Vertex of G by ;
reconsider j = n + 2 as odd Nat ;
take i ; :: thesis: ex n being odd Nat st
( i + 2 < n & n <= len C & C . i <> C . n & C . i in G .AdjacentSet {x} & C . n in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . n,G ) )

take j ; :: thesis: ( i + 2 < j & j <= len C & C . i <> C . j & C . i in G .AdjacentSet {x} & C . j in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . j,G ) )

n + 0 < n + 2 by XREAL_1:8;
hence i + 2 < j ; :: thesis: ( j <= len C & C . i <> C . j & C . i in G .AdjacentSet {x} & C . j in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . j,G ) )

A36: n < len C by ;
hence A37: j <= len C by Th4; :: thesis: ( C . i <> C . j & C . i in G .AdjacentSet {x} & C . j in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . j,G ) )

then reconsider Cj = C . j as Vertex of G by GLIB_001:7;
A38: i in NAT by ORDINAL1:def 12;
A39: now :: thesis: not Ci = xend;
A41: now :: thesis: ( i = 1 implies not j = len C )
assume that
A42: i = 1 and
A43: j = len C ; :: thesis: contradiction
j = i + 4 ;
hence contradiction by A3, A42, A43; :: thesis: verum
end;
hereby :: thesis: ( C . i in G .AdjacentSet {x} & C . j in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . j,G ) )
A44: (i + 2) + (- 2) < j + 0 by XREAL_1:8;
assume C . i = C . j ; :: thesis: contradiction
hence contradiction by A38, A37, A41, A44, GLIB_001:def 28; :: thesis: verum
end;
A45: i < len C by ;
then C . (i + 1) Joins C . i,C . (i + 2),G by ;
then x,Ci are_adjacent by ;
hence C . i in G .AdjacentSet {x} by ; :: thesis: ( C . j in G .AdjacentSet {x} & ( for e being object st e in C .edges() holds
not e Joins C . i,C . j,G ) )

1 + 2 <= j by ;
then A46: j <> 1 ;
A47: n + 2 <= ((len C) - 2) + 2 by ;
A48: now :: thesis: not Cj = xend;
C . (n + 1) Joins C . n,C . j,G by ;
then x,Cj are_adjacent by A5;
hence C . j in G .AdjacentSet {x} by ; :: thesis: for e being object st e in C .edges() holds
not e Joins C . i,C . j,G

let e be object ; :: thesis: ( e in C .edges() implies not e Joins C . i,C . j,G )
assume that
A50: e in C .edges() and
A51: e Joins C . i,C . j,G ; :: thesis: contradiction
consider k being even Element of NAT such that
A52: 1 <= k and
A53: k <= len C and
A54: C . k = e by ;
A55: ( ( (the_Source_of G) . e = C . i & () . e = C . j ) or ( () . e = C . j & () . e = C . i ) ) by A51;
1 + 1 <= k + 1 by ;
then A56: k + 1 <> 1 ;
A57: k - 1 < len C by ;
k in dom C by ;
then consider ku1 being odd Element of NAT such that
A58: ku1 = k - 1 and
k - 1 in dom C and
A59: k + 1 in dom C and
A60: C . k Joins C . ku1,C . (k + 1),G by GLIB_001:9;
A61: k + 1 <= len C by ;
per cases ( ( C . i = C . ku1 & C . j = C . (k + 1) ) or ( C . i = C . (k + 1) & C . j = C . ku1 ) ) by ;
suppose A62: ( C . i = C . ku1 & C . j = C . (k + 1) ) ; :: thesis: contradiction
then i + 2 = (k - 1) + (1 + 1) by
.= j by A37, A61, A46, A56, A62, Th25 ;
hence contradiction ; :: thesis: verum
end;
suppose A63: ( C . i = C . (k + 1) & C . j = C . ku1 ) ; :: thesis: contradiction
per cases ( ( i = k + 1 & j = k - 1 ) or ( i = k + 1 & k - 1 = 1 & j = len C ) or ( i = 1 & k + 1 = len C & j = k - 1 ) or ( i = 1 & k + 1 = len C & k - 1 = 1 & j = len C ) ) by A37, A45, A58, A57, A61, A63, Th25;
suppose ( i = k + 1 & j = k - 1 ) ; :: thesis: contradiction
end;
suppose A64: ( i = k + 1 & k - 1 = 1 & j = len C ) ; :: thesis: contradiction
end;
suppose A65: ( i = 1 & k + 1 = len C & j = k - 1 ) ; :: thesis: contradiction
end;
suppose ( i = 1 & k + 1 = len C & k - 1 = 1 & j = len C ) ; :: thesis: contradiction
end;
end;
end;
end;
end;
end;