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;

now :: thesis: not len P = 1

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

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;

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

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

suppose k < m ; :: thesis: contradiction

hence contradiction by A6, A8, A22, A24, GLIB_001:def 28; :: thesis: verum

end;

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

A27: 1 <= k by ABIAN:12;
k + 2 = 1 by A2, A5, A24, A26, GLIB_001:def 28;
then k + 2 < k + 1 by A27, NAT_1:13;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

suppose k + 2 = n ; :: thesis: contradiction

hence contradiction by A1, A25; :: thesis: verum

end;

suppose A28: k + 2 > n ; :: thesis: contradiction

k + 2 <= len P by A20, Th4;
then n = 1 by A5, A24, A28, GLIB_001:def 28;
hence contradiction by A1, ABIAN:12; :: thesis: verum

end;

end;

end;

suppose k > m ; :: thesis: contradiction

hence contradiction by A6, A22, A20, A24, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

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

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

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;

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

suppose k + 2 < m ; :: thesis: contradiction

hence contradiction by A6, A8, A29, GLIB_001:def 28; :: thesis: verum

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;

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;

end;

end;

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

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

suppose k + 2 < m ; :: thesis: contradiction

hence contradiction by A7, A37, NAT_1:12; :: thesis: verum

end;

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

hence contradiction by A7, A37, NAT_1:12; :: thesis: verum

end;

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

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

end;

end;

end;

suppose k > n ; :: thesis: contradiction

hence contradiction by A5, A22, A20, A29, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

end;