let G be chordal _Graph; :: thesis: for P being Path of G st not P is closed & not P is chordal holds
for x, e being set st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being set holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal )
let P be Path of G; :: thesis: ( not P is closed & not P is chordal implies for x, e being set st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being set holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal ) )
assume A1: ( not P is closed & not P is chordal ) ; :: thesis: for x, e being set st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being set holds not f Joins P . ((len P) - 2),x,G ) holds
( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal )
let x, e be set ; :: thesis: ( not x in P .vertices() & e Joins P .last() ,x,G & ( for f being set holds not f Joins P . ((len P) - 2),x,G ) implies ( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal ) )
assume that
A2: not x in P .vertices() and
A3: e Joins P .last() ,x,G and
A4: for f being set holds not f Joins P . ((len P) - 2),x,G ; :: thesis: ( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal )
reconsider Q = P .addEdge e as Path of G by A1, A2, A3, GLIB_001:152;

A5: now

let n be odd Nat; :: thesis: ( n <= len P implies P . n = Q . n )
assume A6: n <= len P ; :: thesis: P . n = Q . n
( 1 <= n & n <= len P ) by A6, Th2;
then n in dom P by FINSEQ_3:27;
hence P . n = Q . n by A3, GLIB_001:66; :: thesis: verum

end;

A7: ( Q .first() = P .first() & Q .last() = x ) by A3, GLIB_001:64;
then A8: Q .first() in P .vertices() by GLIB_001:89;
A9: len Q = (len P) + 2 by A3, GLIB_001:65;
defpred S₁[ Nat] means ( 4 <= 2 * $1 & 2 * $1 <= (len P) + 1 implies for j being odd Nat st j + (2 * $1) = (len P) + 2 holds
for e being set holds not e Joins Q . j,x,G );
for k being Nat st ( for a being Nat st a < k holds
S₁[a] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for a being Nat st a < k holds
S₁[a] ) implies S₁[k] )
assume A10: for a being Nat st a < k holds
S₁[a] ; :: thesis: S₁[k]
assume A11: ( 4 <= 2 * k & 2 * k <= (len P) + 1 ) ; :: thesis: for j being odd Nat st j + (2 * k) = (len P) + 2 holds
for e being set holds not e Joins Q . j,x,G
let j be odd Nat; :: thesis: ( j + (2 * k) = (len P) + 2 implies for e being set holds not e Joins Q . j,x,G )
assume A12: j + (2 * k) = (len P) + 2 ; :: thesis: for e being set holds not e Joins Q . j,x,G
let e be set ; :: thesis: not e Joins Q . j,x,G
assume A13: e Joins Q . j,x,G ; :: thesis: contradiction
A14: ( k in NAT & j in NAT ) by ORDINAL1:def 13;
j + 4 <= j + (2 * k) by A11, XREAL_1:9;
then A15: (j + 4) - 4 <= ((len P) + 2) - 4 by A12, XREAL_1:11;
A16: (len P) - 2 <= len P by XREAL_1:45;
then A17: j <= len P by A15, XXREAL_0:2;

per cases ( j = (len P) - 2 or j < (len P) - (2 * 1) ) by A15, XXREAL_0:1;

suppose j = (len P) - 2 ; :: thesis: contradiction

then Q . j = P . ((len P) - 2) by A5, XREAL_1:45;
hence contradiction by A4, A13; :: thesis: verum

end;

suppose A18: j < (len P) - (2 * 1) ; :: thesis: contradiction

len P < (len P) + 2 by XREAL_1:31;
then A19: j <= (len P) + 2 by A17, XXREAL_0:2;
reconsider jj = j as odd Element of NAT by ORDINAL1:def 13;
reconsider lP2 = (len P) + 2 as odd Element of NAT ;
set B = Q .cut jj,lP2;
A20: (len (Q .cut jj,lP2)) + j = ((len P) + 2) + 1 by A9, A19, GLIB_001:37;
A21: ((len P) + 3) - ((len P) - 2) < ((len P) + 3) - j by A18, XREAL_1:17;
then A22: 3 < len (Q .cut jj,lP2) by A20, XXREAL_0:2;
A23: ( (Q .cut jj,lP2) .first() = Q . j & (Q .cut jj,lP2) .last() = Q . ((len P) + 2) ) by A9, A19, GLIB_001:38;
A24: ( (Q .cut jj,lP2) .first() = Q . j & (Q .cut jj,lP2) .last() = x ) by A7, A9, A19, GLIB_001:38;
P .vertexAt j = P . j by A17, GLIB_001:def 8;
then P . j in P .vertices() by A14, A15, A16, GLIB_001:90, XXREAL_0:2;
then (Q .cut jj,lP2) .first() in P .vertices() by A5, A15, A16, A23, XXREAL_0:2;
then A25: not Q .cut jj,lP2 is closed by A2, A24, GLIB_001:def 24;

A26: now

let i be even Nat; :: thesis: ( i < (len (Q .cut jj,lP2)) - 1 implies ( (Q .cut jj,lP2) . (i + 1) = P . (j + i) & j + i in dom P ) )
assume A27: i < (len (Q .cut jj,lP2)) - 1 ; :: thesis: ( (Q .cut jj,lP2) . (i + 1) = P . (j + i) & j + i in dom P )
A28: i in NAT by ORDINAL1:def 13;
(len (Q .cut jj,lP2)) - 1 < len (Q .cut jj,lP2) by XREAL_1:46;
then i < len (Q .cut jj,lP2) by A27, XXREAL_0:2;
then A29: ( (Q .cut jj,lP2) . (i + 1) = Q . (j + i) & j + i in dom Q ) by A9, A19, A28, GLIB_001:37;
then A30: ( 1 <= j + i & j + i <= (len P) + 2 ) by A9, FINSEQ_3:27;
j + i < ((len (Q .cut jj,lP2)) - 1) + j by A27, XREAL_1:10;
then j + i <= ((len P) + 2) - 2 by A20, Th3;
hence ( (Q .cut jj,lP2) . (i + 1) = P . (j + i) & j + i in dom P ) by A5, A29, A30, FINSEQ_3:27; :: thesis: verum

end;

set C = (Q .cut jj,lP2) .addEdge e;
A31: e Joins (Q .cut jj,lP2) .last() ,(Q .cut jj,lP2) .first() ,G by A13, A24, GLIB_000:17;

A32: now

let n be odd Nat; :: thesis: ( n <= len (Q .cut jj,lP2) implies ((Q .cut jj,lP2) .addEdge e) . n = (Q .cut jj,lP2) . n )
assume A33: n <= len (Q .cut jj,lP2) ; :: thesis: ((Q .cut jj,lP2) .addEdge e) . n = (Q .cut jj,lP2) . n
( 1 <= n & n <= len (Q .cut jj,lP2) ) by A33, Th2;
then n in dom (Q .cut jj,lP2) by FINSEQ_3:27;
hence ((Q .cut jj,lP2) .addEdge e) . n = (Q .cut jj,lP2) . n by A31, GLIB_001:66; :: thesis: verum

end;

A34: (Q .cut jj,lP2) .addEdge e is Cycle-like by A13, A22, A24, A25, Th33, GLIB_000:17;
A35: ( ((Q .cut jj,lP2) .addEdge e) .first() = Q . j & ((Q .cut jj,lP2) .addEdge e) .last() = Q . j ) by A23, A31, GLIB_001:64;
A36: len ((Q .cut jj,lP2) .addEdge e) = (len (Q .cut jj,lP2)) + 2 by A13, A24, GLIB_000:17, GLIB_001:65;
(len (Q .cut jj,lP2)) + 2 > 5 + 2 by A20, A21, XREAL_1:10;
then A37: len ((Q .cut jj,lP2) .addEdge e) > 7 by A13, A24, GLIB_000:17, GLIB_001:65;

now

assume ((Q .cut jj,lP2) .addEdge e) .length() <= 3 ; :: thesis: contradiction
then 2 * (((Q .cut jj,lP2) .addEdge e) .length() ) <= 2 * 3 by XREAL_1:66;
then (2 * (((Q .cut jj,lP2) .addEdge e) .length() )) + 1 <= (2 * 3) + 1 by XREAL_1:8;
hence contradiction by A37, GLIB_001:113; :: thesis: verum

end;

then (Q .cut jj,lP2) .addEdge e is chordal by A34, Def11;
then consider m, n being odd Nat such that
A38: ( m + 2 < n & n <= len ((Q .cut jj,lP2) .addEdge e) & ((Q .cut jj,lP2) .addEdge e) . m <> ((Q .cut jj,lP2) .addEdge e) . n ) and
A39: ex e being set st e Joins ((Q .cut jj,lP2) .addEdge e) . m,((Q .cut jj,lP2) .addEdge e) . n,G and
A40: ( (Q .cut jj,lP2) .addEdge e is Cycle-like implies ( ( not m = 1 or not n = len ((Q .cut jj,lP2) .addEdge e) ) & ( not m = 1 or not n = (len ((Q .cut jj,lP2) .addEdge e)) - 2 ) & ( not m = 3 or not n = len ((Q .cut jj,lP2) .addEdge e) ) ) ) by Th84;
consider e being set such that
A41: e Joins ((Q .cut jj,lP2) .addEdge e) . m,((Q .cut jj,lP2) .addEdge e) . n,G by A39;
1 <= m by Th2;
then 1 - 1 <= m - 1 by XREAL_1:11;
then reconsider m1 = m - 1 as even Element of NAT by INT_1:16;
reconsider m1 = m1 as even Nat ;
1 <= n by Th2;
then 1 - 1 <= n - 1 by XREAL_1:11;
then reconsider n1 = n - 1 as even Element of NAT by INT_1:16;
reconsider n1 = n1 as even Nat ;
m < m + 2 by XREAL_1:31;
then m < n by A38, XXREAL_0:2;
then A42: m1 < n1 by XREAL_1:11;
A43: (m + 2) - 1 < n - 1 by A38, XREAL_1:11;
m + 2 < (len (Q .cut jj,lP2)) + 2 by A36, A38, XXREAL_0:2;
then A44: (m + 2) - 2 < ((len (Q .cut jj,lP2)) + 2) - 2 by XREAL_1:11;
then m1 < (len (Q .cut jj,lP2)) - 1 by XREAL_1:11;
then A45: ( (Q .cut jj,lP2) . (m1 + 1) = P . (j + m1) & j + m1 in dom P ) by A26;
then A46: ( (Q .cut jj,lP2) . m = P . (j + m1) & j + m1 <= len P ) by FINSEQ_3:27;

now

assume A47: n = len ((Q .cut jj,lP2) .addEdge e) ; :: thesis: contradiction
then e Joins P . (j + m1),Q . j,G by A32, A35, A41, A44, A45;
then e Joins P . (j + m1),P . j,G by A5, A15, A16, XXREAL_0:2;
then A48: e Joins P . j,P . (j + m1),G by GLIB_000:17;

now

assume m <= 3 ; :: thesis: contradiction
then m <= 4 by XXREAL_0:2;
hence contradiction by A22, A25, A31, A40, A47, Th7, Th33; :: thesis: verum

end;

then A49: (2 + 1) - 1 < m - 1 by XREAL_1:11;
then A50: j + 2 < j + m1 by XREAL_1:10;
j < j + m1 by A49, XREAL_1:31;
hence contradiction by A1, A46, A48, A50, Th92; :: thesis: verum

end;

then n < (len (Q .cut jj,lP2)) + (2 * 1) by A36, A38, XXREAL_0:1;
then A51: n <= ((len (Q .cut jj,lP2)) + 2) - 2 by Th3;

now

assume A52: n = len (Q .cut jj,lP2) ; :: thesis: contradiction
then A53: ((Q .cut jj,lP2) .addEdge e) . n = x by A24, A32;
( 1 <> m & 1 <= m ) by A22, A25, A31, A36, A40, A52, Th2, Th33;
then 1 < m by XXREAL_0:1;
then A54: 1 - 1 < m - 1 by XREAL_1:11;
( j + m1 <= len P & len P < (len P) + 2 ) by A45, FINSEQ_3:27, XREAL_1:31;
then j + m1 < (len P) + (2 * 1) by XXREAL_0:2;
then consider kk being Nat such that
A55: (j + m1) + (2 * kk) = (len P) + 2 by Lm2;

A56: now

assume 2 * kk < 3 + 1 ; :: thesis: contradiction
then 2 * kk <= 3 by NAT_1:13;
then ( 2 * kk = 0 or 2 * kk = 2 ) by Th11;
hence contradiction by A20, A38, A52, A55; :: thesis: verum

end;

A57: now

assume 2 * kk > (len P) + 1 ; :: thesis: contradiction
then A58: 2 * kk >= ((len P) + 1) + 1 by NAT_1:13;
( (2 * kk) + m1 > 2 * kk & ((2 * kk) + m1) + j >= (2 * kk) + m1 ) by A54, NAT_1:11, XREAL_1:31;
hence contradiction by A55, A58, XXREAL_0:2; :: thesis: verum

end;

A59: now

assume kk >= k ; :: thesis: contradiction
then A60: 2 * kk >= 2 * k by XREAL_1:66;
(j + (2 * kk)) + m1 > j + (2 * kk) by A54, XREAL_1:31;
hence contradiction by A12, A55, A60, XREAL_1:9; :: thesis: verum

end;

((Q .cut jj,lP2) .addEdge e) . m = (Q .cut jj,lP2) . m by A32, A44;
then ((Q .cut jj,lP2) .addEdge e) . m = Q . (j + m1) by A5, A46;
hence contradiction by A10, A41, A53, A55, A56, A57, A59; :: thesis: verum

end;

then n < len (Q .cut jj,lP2) by A51, XXREAL_0:1;
then n1 < (len (Q .cut jj,lP2)) - 1 by XREAL_1:11;
then ( (Q .cut jj,lP2) . (n1 + 1) = P . (j + n1) & j + n1 in dom P ) by A26;
then A61: ( (Q .cut jj,lP2) . n = P . (j + n1) & j + n1 <= len P ) by FINSEQ_3:27;
A62: ( ((Q .cut jj,lP2) .addEdge e) . m = (Q .cut jj,lP2) . m & ((Q .cut jj,lP2) .addEdge e) . n = (Q .cut jj,lP2) . n ) by A32, A44, A51;
A63: j + m1 < j + n1 by A42, XREAL_1:10;
j + (m1 + 2) < j + n1 by A43, XREAL_1:10;
then (j + m1) + 2 < j + n1 ;
hence contradiction by A1, A41, A45, A61, A62, A63, Th92; :: thesis: verum

end;

end;

end;

then A64: for k being Nat st ( for a being Nat st a < k holds
S₁[a] ) holds
S₁[k] ;
A65: for k being Nat holds S₁[k] from NAT_1:sch 4(A64);

A66: now

let n be odd Nat; :: thesis: ( n <= (len P) - 2 implies for e being set holds not e Joins Q . n,x,G )
assume A67: n <= (len P) - 2 ; :: thesis: for e being set holds not e Joins Q . n,x,G
(len P) - 2 <= ((len P) - 2) + 4 by XREAL_1:33;
then n <= (len P) + (2 * 1) by A67, XXREAL_0:2;
then consider k being Nat such that
A68: n + (2 * k) = (len P) + 2 by Lm2;

A69: now

assume A70: 2 * k < 4 ; :: thesis: contradiction
n + 4 <= ((len P) - 2) + 4 by A67, XREAL_1:9;
hence contradiction by A68, A70, XREAL_1:10; :: thesis: verum

end;

now

assume A71: 2 * k > (len P) + 1 ; :: thesis: contradiction
1 <= n by Th2;
then n + (2 * k) > 1 + ((len P) + 1) by A71, XREAL_1:10;
hence contradiction by A68; :: thesis: verum

end;

hence for e being set holds not e Joins Q . n,x,G by A65, A68, A69; :: thesis: verum

end;

now

assume Q is chordal ; :: thesis: contradiction
then consider m, n being odd Nat such that
A72: ( m + 2 < n & n <= len Q & Q . m <> Q . n ) and
A73: ex e being set st e Joins Q . m,Q . n,G and
( Q is Cycle-like implies ( ( not m = 1 or not n = len Q ) & ( not m = 1 or not n = (len Q) - 2 ) & ( not m = 3 or not n = len Q ) ) ) by Th84;
consider e being set such that
A74: e Joins Q . m,Q . n,G by A73;
m < m + 2 by XREAL_1:31;
then A75: m < n by A72, XXREAL_0:2;
m + 2 < (len P) + 2 by A9, A72, XXREAL_0:2;
then A76: (m + 2) - 2 < ((len P) + 2) - 2 by XREAL_1:11;

per cases ( n = len Q or n < len Q ) by A72, XXREAL_0:1;

suppose A77: n = len Q ; :: thesis: contradiction

then (m + 2) - 2 < ((len P) + 2) - 2 by A9, A72, XREAL_1:11;
hence contradiction by A7, A66, A74, A77, Th3; :: thesis: verum

end;

suppose n < len Q ; :: thesis: contradiction

then A78: n <= ((len P) + 2) - 2 by A9, Th3;
then ( Q . m = P . m & Q . n = P . n ) by A5, A76;
hence contradiction by A1, A72, A74, A75, A78, Th92; :: thesis: verum

end;

end;

end;

hence ( P .addEdge e is Path-like & not P .addEdge e is closed & not P .addEdge e is chordal ) by A2, A7, A8, GLIB_001:def 24; :: thesis: verum