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 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: ( 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;

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 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: ( 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 ) )
;

end;

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 ) )

( 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 ;

(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 ;

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 A3, XREAL_1:7;

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 A9, XXREAL_0:2;

then A11: i < len C by A10, XXREAL_0:2;

then reconsider Ci = C . i as Vertex of G by GLIB_001:7;

(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 A14: x,Ci are_adjacent by A8;

x <> Ci by A13, A8, GLIB_001:def 28;

hence C . i in G .AdjacentSet {x} by A14, Th51; :: 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 A10, GLIB_001:7;

then x,Cj are_adjacent by A17, Def3;

hence C . j in G .AdjacentSet {x} by A18, Th51; :: 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 A20, GLIB_001:99;

A25: ( ( (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 ) ) by A21;

k in dom C by A22, A23, FINSEQ_3:25;

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 A26, A27, FINSEQ_3:25;

A31: k + 1 <= len C by A28, FINSEQ_3:25;

end;(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 ;

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 A3, XREAL_1:7;

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 A9, XXREAL_0:2;

then A11: i < len C by A10, XXREAL_0:2;

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 ) )

A13:
(len C) + 0 > 9 + (- 6)
by A3, XREAL_1:8;not e Joins C . i,C . j,G ) )

assume A12:
C . i = C . j
; :: thesis: contradiction

(i + 2) + (- 2) < j + 0 by A9, XXREAL_0:2;

hence contradiction by A10, A12, GLIB_001:def 28; :: thesis: verum

end;(i + 2) + (- 2) < j + 0 by A9, XXREAL_0:2;

hence contradiction by A10, A12, GLIB_001:def 28; :: thesis: verum

then reconsider Ci = C . i as Vertex of G by GLIB_001:7;

(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 A14: x,Ci are_adjacent by A8;

x <> Ci by A13, A8, GLIB_001:def 28;

hence C . i in G .AdjacentSet {x} by A14, Th51; :: 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 A10, GLIB_001:7;

A18: now :: thesis: not x = Cj

C . (j + 1) Joins C . j,C . (j + 2),G
by A16, A10, GLIB_001:def 3;assume
x = Cj
; :: thesis: contradiction

then A19: j = 1 by A16, A10, A17, GLIB_001:def 28;

j + 2 = len C ;

hence contradiction by A3, A19; :: thesis: verum

end;then A19: j = 1 by A16, A10, A17, GLIB_001:def 28;

j + 2 = len C ;

hence contradiction by A3, A19; :: thesis: verum

then x,Cj are_adjacent by A17, Def3;

hence C . j in G .AdjacentSet {x} by A18, Th51; :: 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 A20, GLIB_001:99;

A25: ( ( (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 ) ) by A21;

k in dom C by A22, A23, FINSEQ_3:25;

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 A26, A27, FINSEQ_3:25;

A31: k + 1 <= len C by A28, FINSEQ_3:25;

per cases
( ( C . i = C . ku1 & C . j = C . (k + 1) ) or ( C . i = C . (k + 1) & C . j = C . ku1 ) )
by A24, A29, A25;

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 ) )

( 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 A6, XXREAL_0:1;

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 A4, GLIB_001:7, XXREAL_0:2;

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 A4, A34, XXREAL_0:1;

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;

then C . (i + 1) Joins C . i,C . (i + 2),G by A38, GLIB_001:def 3;

then x,Ci are_adjacent by A5, Def3;

hence C . i in G .AdjacentSet {x} by A39, Th51; :: 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 A6, XREAL_1:7;

then A46: j <> 1 ;

A47: n + 2 <= ((len C) - 2) + 2 by A36, Th4;

then x,Cj are_adjacent by A5;

hence C . j in G .AdjacentSet {x} by A48, Th51; :: 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 A50, GLIB_001:99;

A55: ( ( (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 ) ) by A51;

1 + 1 <= k + 1 by A52, XREAL_1:7;

then A56: k + 1 <> 1 ;

A57: k - 1 < len C by A53, XREAL_1:146, XXREAL_0:2;

k in dom C by A52, A53, FINSEQ_3:25;

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 A59, FINSEQ_3:25;

end;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 A4, GLIB_001:7, XXREAL_0:2;

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 A4, A34, XXREAL_0:1;

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 = x

A40:
n + 0 > n + (- 2)
by XREAL_1:8;

assume Ci = x ; :: thesis: contradiction

hence contradiction by A4, A5, A34, A38, A40, GLIB_001:def 28; :: thesis: verum

end;assume Ci = x ; :: thesis: contradiction

hence contradiction by A4, A5, A34, A38, A40, GLIB_001:def 28; :: thesis: verum

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;A42: i = 1 and

A43: j = len C ; :: thesis: contradiction

j = i + 4 ;

hence contradiction by A3, A42, A43; :: thesis: verum

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 ) )

A45:
i < len C
by A4, A35, XXREAL_0:2;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;assume C . i = C . j ; :: thesis: contradiction

hence contradiction by A38, A37, A41, A44, GLIB_001:def 28; :: thesis: verum

then C . (i + 1) Joins C . i,C . (i + 2),G by A38, GLIB_001:def 3;

then x,Ci are_adjacent by A5, Def3;

hence C . i in G .AdjacentSet {x} by A39, Th51; :: 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 A6, XREAL_1:7;

then A46: j <> 1 ;

A47: n + 2 <= ((len C) - 2) + 2 by A36, Th4;

A48: now :: thesis: not Cj = x

C . (n + 1) Joins C . n,C . j,G
by A36, GLIB_001:def 3;A49:
n + 2 > n + 0
by XREAL_1:8;

assume Cj = x ; :: thesis: contradiction

hence contradiction by A5, A34, A47, A49, GLIB_001:def 28; :: thesis: verum

end;assume Cj = x ; :: thesis: contradiction

hence contradiction by A5, A34, A47, A49, GLIB_001:def 28; :: thesis: verum

then x,Cj are_adjacent by A5;

hence C . j in G .AdjacentSet {x} by A48, Th51; :: 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 A50, GLIB_001:99;

A55: ( ( (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 ) ) by A51;

1 + 1 <= k + 1 by A52, XREAL_1:7;

then A56: k + 1 <> 1 ;

A57: k - 1 < len C by A53, XREAL_1:146, XXREAL_0:2;

k in dom C by A52, A53, FINSEQ_3:25;

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 A59, FINSEQ_3:25;

per cases
( ( C . i = C . ku1 & C . j = C . (k + 1) ) or ( C . i = C . (k + 1) & C . j = C . ku1 ) )
by A54, A60, A55;

end;

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

then i + 2 =
(k - 1) + (1 + 1)
by A45, A58, A57, Th25

.= j by A37, A61, A46, A56, A62, Th25 ;

hence contradiction ; :: thesis: verum

end;.= j by A37, A61, A46, A56, A62, Th25 ;

hence contradiction ; :: thesis: verum

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

end;

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;

end;