let G be _Graph; 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; ( 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
; 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; ( 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()
; 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 )
;
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 ;
(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
;
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
;
( 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;
( 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
;
( 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;
A13:
(len C) + 0 > 9
+ (- 6)
by A3, XREAL_1:8;
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;
( 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;
C . (j + 1) Joins C . j,
C . (j + 2),
G
by A16, A10, GLIB_001:def 3;
then
x,
Cj are_adjacent
by A17, Def3;
hence
C . j in G .AdjacentSet {x}
by A18, Th51;
for e being object st e in C .edges() holds
not e Joins C . i,C . j,Glet e be
object ;
( 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
;
contradictionconsider 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; suppose A34:
( not
n = 1 & not
n = len C )
;
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 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
;
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
;
( 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
;
( 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;
( 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;
A41:
now ( i = 1 implies not j = len C )assume that A42:
i = 1
and A43:
j = len C
;
contradiction
j = i + 4
;
hence
contradiction
by A3, A42, A43;
verum end; A45:
i < len C
by A4, A35, XXREAL_0:2;
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;
( 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;
C . (n + 1) Joins C . n,
C . j,
G
by A36, GLIB_001:def 3;
then
x,
Cj are_adjacent
by A5;
hence
C . j in G .AdjacentSet {x}
by A48, Th51;
for e being object st e in C .edges() holds
not e Joins C . i,C . j,Glet e be
object ;
( 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
;
contradictionconsider 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; end;