let G be _Graph; :: thesis: 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; :: thesis: ( 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 ) ) ) ; :: thesis: P is chordal

A5: n in NAT by ORDINAL1:def 12;

take m ; :: according to CHORD:def 10 :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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;

not f Joins P . m,P . n,G

let f be object ; :: thesis: ( 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 ; :: thesis: 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;

( 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; :: thesis: ( 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 ) ) ) ; :: thesis: P is chordal

A5: n in NAT by ORDINAL1:def 12;

take m ; :: according to CHORD:def 10 :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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;

now :: thesis: not len P = 1

then A9:
not P is trivial
by GLIB_001:126;assume
len P = 1
; :: thesis: contradiction

then m + 2 < 1 by A1, A2, XXREAL_0:2;

hence contradiction by NAT_1:12; :: thesis: verum

end;then m + 2 < 1 by A1, A2, XXREAL_0:2;

hence contradiction by NAT_1:12; :: thesis: verum

hereby :: thesis: ( 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
ex e being object st e Joins P . m,P . n,G
by A3; :: thesis: for f being object st f in P .edges() holds not f Joins P . m,P . n,G ) )

assume A10:
P . m = P . n
; :: thesis: contradiction

then 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; :: thesis: verum

end;then 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; :: thesis: verum

not f Joins P . m,P . n,G

let f be object ; :: thesis: ( 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 ; :: thesis: 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;

end;

suppose A24:
( P . k = P . m & P . (k + 2) = P . n )
; :: thesis: contradiction

end;

per cases
( k < m or k = m or k > m )
by XXREAL_0:1;

end;

suppose A25:
k = m
; :: thesis: contradiction

end;

suppose A29:
( P . k = P . n & P . (k + 2) = P . m )
; :: thesis: contradiction

end;

per cases
( k < n or k = n or k > n )
by XXREAL_0:1;

end;

suppose A30:
k < n
; :: thesis: contradiction

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

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

end;

suppose A33:
k + 2 = m
; :: thesis: contradiction

P is closed
by A29, A32, A31;

hence contradiction by A2, A4, A5, A9, A29, A30, A32, A33, GLIB_001:def 28; :: thesis: verum

end;hence contradiction by A2, A4, A5, A9, A29, A30, A32, A33, GLIB_001:def 28; :: thesis: verum

suppose A34:
k + 2 > m
; :: thesis: contradiction

A35:
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; :: thesis: verum

end;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; :: thesis: verum

suppose A37:
k = n
; :: thesis: contradiction

end;