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 ;
then A8: m < len P by ;
now :: thesis: not len P = 1
assume len P = 1 ; :: thesis: contradiction
then m + 2 < 1 by ;
hence contradiction by NAT_1:12; :: thesis: verum
end;
then A9: not P is trivial by GLIB_001:126;
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 ) )
end;
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

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 () and
A15: (P .edgeSeq()) . i = f by ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
set k = (2 * i) - 1;
A16: 1 <= i by ;
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 () by ;
then A18: (P .edgeSeq()) . i = P . (2 * i) by ;
reconsider k = (2 * i) - 1 as odd Nat by A17;
2 * i in dom P by ;
then A19: 2 * i <= len P by FINSEQ_3:25;
k + 1 = 2 * i ;
then A20: k < len P by ;
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 ;
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 ) ; :: thesis: contradiction
per cases ( k < m or k = m or k > m ) by XXREAL_0:1;
suppose A25: k = m ; :: thesis: contradiction
per cases ( k + 2 < n or k + 2 = n or k + 2 > n ) by XXREAL_0:1;
suppose A26: k + 2 < n ; :: thesis: contradiction
end;
suppose A28: k + 2 > n ; :: thesis: contradiction
end;
end;
end;
end;
end;
suppose A29: ( P . k = P . n & P . (k + 2) = P . m ) ; :: thesis: contradiction
end;
end;