let G be _Graph; for P being Path of G st ex m, n being odd Nat st
( m + 2 < n & n <= len P & ex e being object st e Joins P . m,P . n,G & ( P is Cycle-like implies ( ( not m = 1 or not n = len P ) & ( not m = 1 or not n = (len P) - 2 ) & ( not m = 3 or not n = len P ) ) ) ) holds
P is chordal
let P be Path of G; ( ex m, n being odd Nat st
( m + 2 < n & n <= len P & ex e being object st e Joins P . m,P . n,G & ( P is Cycle-like implies ( ( not m = 1 or not n = len P ) & ( not m = 1 or not n = (len P) - 2 ) & ( not m = 3 or not n = len P ) ) ) ) implies P is chordal )
given m, n being odd Nat such that A1:
m + 2 < n
and
A2:
n <= len P
and
A3:
ex e being object st e Joins P . m,P . n,G
and
A4:
( P is Cycle-like implies ( ( not m = 1 or not n = len P ) & ( not m = 1 or not n = (len P) - 2 ) & ( not m = 3 or not n = len P ) ) )
; P is chordal
A5:
n in NAT
by ORDINAL1:def 12;
take
m
; CHORD:def 10 ex n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G ) )
take
n
; ( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G ) )
thus
m + 2 < n
by A1; ( n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G ) )
thus
n <= len P
by A2; ( P . m <> P . n & ex e being object st e Joins P . m,P . n,G & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G ) )
A6:
m in NAT
by ORDINAL1:def 12;
A7:
m < n
by A1, NAT_1:12;
then A8:
m < len P
by A2, XXREAL_0:2;
then A9:
P is V5()
by GLIB_001:126;
hereby ( ex e being object st e Joins P . m,P . n,G & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G ) )
assume A10:
P . m = P . n
;
contradictionthen A11:
n = len P
by A2, A6, A5, A7, GLIB_001:def 28;
m = 1
by A2, A6, A5, A7, A10, GLIB_001:def 28;
then
P is
closed
by A10, A11;
hence
contradiction
by A2, A4, A6, A5, A7, A9, A10, GLIB_001:def 28;
verum
end;
thus
ex e being object st e Joins P . m,P . n,G
by A3; for f being object st f in P .edges() holds
not f Joins P . m,P . n,G
let f be object ; ( f in P .edges() implies not f Joins P . m,P . n,G )
assume that
A12:
f in P .edges()
and
A13:
f Joins P . m,P . n,G
; contradiction
consider i being Nat such that
A14:
i in dom (P .edgeSeq())
and
A15:
(P .edgeSeq()) . i = f
by A12, FINSEQ_2:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
set k = (2 * i) - 1;
A16:
1 <= i
by A14, FINSEQ_3:25;
then
2 * 1 <= 2 * i
by XREAL_1:64;
then
2 - 1 <= (2 * i) - 1
by XREAL_1:9;
then A17:
(2 * i) - 1 is Element of NAT
by INT_1:3;
i <= len (P .edgeSeq())
by A14, FINSEQ_3:25;
then A18:
(P .edgeSeq()) . i = P . (2 * i)
by A16, GLIB_001:def 15;
reconsider k = (2 * i) - 1 as odd Nat by A17;
2 * i in dom P
by A14, GLIB_001:78;
then A19:
2 * i <= len P
by FINSEQ_3:25;
k + 1 = 2 * i
;
then A20:
k < len P
by A19, NAT_1:13;
then A21:
k + 2 <= len P
by Th4;
A22:
k in NAT
by ORDINAL1:def 12;
then A23:
P . (k + 1) Joins P . k,P . (k + 2),G
by A20, GLIB_001:def 3;
per cases
( ( P . k = P . m & P . (k + 2) = P . n ) or ( P . k = P . n & P . (k + 2) = P . m ) )
by A13, A15, A18, A23;
suppose A24:
(
P . k = P . m &
P . (k + 2) = P . n )
;
contradictionend; suppose A29:
(
P . k = P . n &
P . (k + 2) = P . m )
;
contradictionper cases
( k < n or k = n or k > n )
by XXREAL_0:1;
suppose A30:
k < n
;
contradictionthen A31:
n = len P
by A2, A5, A22, A29, GLIB_001:def 28;
A32:
k = 1
by A2, A5, A22, A29, A30, GLIB_001:def 28;
per cases
( k + 2 < m or k + 2 = m or k + 2 > m )
by XXREAL_0:1;
suppose A33:
k + 2
= m
;
contradiction
P is
closed
by A29, A32, A31;
hence
contradiction
by A2, A4, A5, A9, A29, A30, A32, A33, GLIB_001:def 28;
verum end; suppose A34:
k + 2
> m
;
contradictionA35:
k + 2
<= n
by A30, Th4;
A36:
k + 2
= len P
by A6, A21, A29, A34, GLIB_001:def 28;
m = 1
by A6, A21, A29, A34, GLIB_001:def 28;
then
P is
closed
by A29, A36;
hence
contradiction
by A2, A4, A6, A9, A29, A34, A36, A35, GLIB_001:def 28, XXREAL_0:1;
verum end; end; end; suppose A37:
k = n
;
contradictionper cases
( k + 2 < m or k + 2 = m or k + 2 > m )
by XXREAL_0:1;
suppose A38:
k + 2
> m
;
contradictionA39:
k + 2
= len P
by A6, A21, A29, A38, GLIB_001:def 28;
m = 1
by A6, A21, A29, A38, GLIB_001:def 28;
then
P is
closed
by A29, A39;
hence
contradiction
by A4, A6, A9, A29, A37, A38, A39, GLIB_001:def 28;
verum end; end; end; end; end; end;