let G be chordal _Graph; :: thesis: for P being Path of G st P is open & P is chordless holds

for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) holds

( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )

let P be Path of G; :: thesis: ( P is open & P is chordless implies for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) holds

( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless ) )

assume that

A1: P is open and

A2: P is chordless ; :: thesis: for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) holds

( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )

let x, e be object ; :: thesis: ( not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) implies ( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless ) )

assume that

A3: not x in P .vertices() and

A4: e Joins P .last() ,x,G and

A5: for f being object holds not f Joins P . ((len P) - 2),x,G ; :: thesis: ( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )

reconsider Q = P .addEdge e as Path of G by A1, A3, A4, GLIB_001:151;

A6: len Q = (len P) + 2 by A4, GLIB_001:64;

defpred S_{1}[ 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 object holds not e Joins Q . j,x,G );

for k being Nat st ( for a being Nat st a < k holds

S_{1}[a] ) holds

S_{1}[k]

S_{1}[a] ) holds

S_{1}[k]
;

A72: for k being Nat holds S_{1}[k]
from NAT_1:sch 4(A71);

then Q .first() in P .vertices() by GLIB_001:88;

hence ( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless ) by A3, A9, A78; :: thesis: verum

for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) holds

( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )

let P be Path of G; :: thesis: ( P is open & P is chordless implies for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) holds

( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless ) )

assume that

A1: P is open and

A2: P is chordless ; :: thesis: for x, e being object st not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) holds

( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )

let x, e be object ; :: thesis: ( not x in P .vertices() & e Joins P .last() ,x,G & ( for f being object holds not f Joins P . ((len P) - 2),x,G ) implies ( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless ) )

assume that

A3: not x in P .vertices() and

A4: e Joins P .last() ,x,G and

A5: for f being object holds not f Joins P . ((len P) - 2),x,G ; :: thesis: ( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless )

reconsider Q = P .addEdge e as Path of G by A1, A3, A4, GLIB_001:151;

A6: len Q = (len P) + 2 by A4, GLIB_001:64;

defpred S

for e being object holds not e Joins Q . j,x,G );

A7: now :: thesis: for n being odd Nat st n <= len P holds

P . n = Q . n

A9:
Q .last() = x
by A4, GLIB_001:63;P . n = Q . n

let n be odd Nat; :: thesis: ( n <= len P implies P . n = Q . n )

assume A8: n <= len P ; :: thesis: P . n = Q . n

1 <= n by Th2;

then n in dom P by A8, FINSEQ_3:25;

hence P . n = Q . n by A4, GLIB_001:65; :: thesis: verum

end;assume A8: n <= len P ; :: thesis: P . n = Q . n

1 <= n by Th2;

then n in dom P by A8, FINSEQ_3:25;

hence P . n = Q . n by A4, GLIB_001:65; :: thesis: verum

for k being Nat st ( for a being Nat st a < k holds

S

S

proof

then A71:
for k being Nat st ( for a being Nat st a < k holds
let k be Nat; :: thesis: ( ( for a being Nat st a < k holds

S_{1}[a] ) implies S_{1}[k] )

assume A10: for a being Nat st a < k holds

S_{1}[a]
; :: thesis: S_{1}[k]

assume that

A11: 4 <= 2 * k and

2 * k <= (len P) + 1 ; :: thesis: for j being odd Nat st j + (2 * k) = (len P) + 2 holds

for e being object holds not e Joins Q . j,x,G

let j be odd Nat; :: thesis: ( j + (2 * k) = (len P) + 2 implies for e being object holds not e Joins Q . j,x,G )

assume A12: j + (2 * k) = (len P) + 2 ; :: thesis: for e being object holds not e Joins Q . j,x,G

j + 4 <= j + (2 * k) by A11, XREAL_1:7;

then A13: (j + 4) - 4 <= ((len P) + 2) - 4 by A12, XREAL_1:9;

A14: (len P) - 2 <= len P by XREAL_1:43;

then A15: j <= len P by A13, XXREAL_0:2;

A16: j in NAT by ORDINAL1:def 12;

let e be object ; :: thesis: not e Joins Q . j,x,G

assume A17: e Joins Q . j,x,G ; :: thesis: contradiction

end;S

assume A10: for a being Nat st a < k holds

S

assume that

A11: 4 <= 2 * k and

2 * k <= (len P) + 1 ; :: thesis: for j being odd Nat st j + (2 * k) = (len P) + 2 holds

for e being object holds not e Joins Q . j,x,G

let j be odd Nat; :: thesis: ( j + (2 * k) = (len P) + 2 implies for e being object holds not e Joins Q . j,x,G )

assume A12: j + (2 * k) = (len P) + 2 ; :: thesis: for e being object holds not e Joins Q . j,x,G

j + 4 <= j + (2 * k) by A11, XREAL_1:7;

then A13: (j + 4) - 4 <= ((len P) + 2) - 4 by A12, XREAL_1:9;

A14: (len P) - 2 <= len P by XREAL_1:43;

then A15: j <= len P by A13, XXREAL_0:2;

A16: j in NAT by ORDINAL1:def 12;

let e be object ; :: thesis: not e Joins Q . j,x,G

assume A17: e Joins Q . j,x,G ; :: thesis: contradiction

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

end;

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

reconsider lP2 = (len P) + 2 as odd Element of NAT ;

reconsider jj = j as odd Element of NAT by ORDINAL1:def 12;

set B = Q .cut (jj,lP2);

len P < (len P) + 2 by XREAL_1:29;

then A19: j <= (len P) + 2 by A15, XXREAL_0:2;

then A20: (Q .cut (jj,lP2)) .last() = x by A9, A6, GLIB_001:37;

A21: (len (Q .cut (jj,lP2))) + j = ((len P) + 2) + 1 by A6, A19, GLIB_001:36;

A28: (Q .cut (jj,lP2)) .first() = Q . j by A6, A19, GLIB_001:37;

A29: (Q .cut (jj,lP2)) .first() = Q . j by A6, A19, GLIB_001:37;

then A30: e Joins (Q .cut (jj,lP2)) .last() ,(Q .cut (jj,lP2)) .first() ,G by A17, A20;

then A34: 3 < len (Q .cut (jj,lP2)) by A21, XXREAL_0:2;

(len (Q .cut (jj,lP2))) + 2 > 5 + 2 by A21, A33, XREAL_1:8;

then A35: len ((Q .cut (jj,lP2)) .addEdge e) > 7 by A17, A20, GLIB_000:14, GLIB_001:64;

then P . j in P .vertices() by A16, A13, A14, GLIB_001:89, XXREAL_0:2;

then (Q .cut (jj,lP2)) .first() in P .vertices() by A7, A13, A14, A28, XXREAL_0:2;

then A37: Q .cut (jj,lP2) is open by A3, A20;

then (Q .cut (jj,lP2)) .addEdge e is Cycle-like by A17, A34, A29, A20, Th33, GLIB_000:14;

then (Q .cut (jj,lP2)) .addEdge e is chordal by A36, Def11;

then consider m, n being odd Nat such that

A38: m + 2 < n and

A39: n <= len ((Q .cut (jj,lP2)) .addEdge e) and

A40: ((Q .cut (jj,lP2)) .addEdge e) . m <> ((Q .cut (jj,lP2)) .addEdge e) . n and

A41: ex e being object st e Joins ((Q .cut (jj,lP2)) .addEdge e) . m,((Q .cut (jj,lP2)) .addEdge e) . n,G and

A42: ( (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 Th83;

consider e being object such that

A43: e Joins ((Q .cut (jj,lP2)) .addEdge e) . m,((Q .cut (jj,lP2)) .addEdge e) . n,G by A41;

1 <= m by Th2;

then 1 - 1 <= m - 1 by XREAL_1:9;

then reconsider m1 = m - 1 as even Element of NAT by INT_1:3;

reconsider m1 = m1 as even Nat ;

A44: len ((Q .cut (jj,lP2)) .addEdge e) = (len (Q .cut (jj,lP2))) + 2 by A17, A20, GLIB_000:14, GLIB_001:64;

then m + 2 < (len (Q .cut (jj,lP2))) + 2 by A38, A39, XXREAL_0:2;

then A45: (m + 2) - 2 < ((len (Q .cut (jj,lP2))) + 2) - 2 by XREAL_1:9;

then A46: m1 < (len (Q .cut (jj,lP2))) - 1 by XREAL_1:9;

then A47: (Q .cut (jj,lP2)) . (m1 + 1) = P . (j + m1) by A22;

A48: j + m1 in dom P by A22, A46;

then A49: j + m1 <= len P by FINSEQ_3:25;

A50: ((Q .cut (jj,lP2)) .addEdge e) .last() = Q . j by A28, A30, GLIB_001:63;

then A55: n <= ((len (Q .cut (jj,lP2))) + 2) - 2 by Th3;

then A56: ((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n by A31;

1 <= n by Th2;

then 1 - 1 <= n - 1 by XREAL_1:9;

then reconsider n1 = n - 1 as even Element of NAT by INT_1:3;

reconsider n1 = n1 as even Nat ;

(m + 2) - 1 < n - 1 by A38, XREAL_1:9;

then j + (m1 + 2) < j + n1 by XREAL_1:8;

then A57: (j + m1) + 2 < j + n1 ;

then A67: n1 < (len (Q .cut (jj,lP2))) - 1 by XREAL_1:9;

then j + n1 in dom P by A22;

then A68: j + n1 <= len P by FINSEQ_3:25;

m < m + 2 by XREAL_1:29;

then m < n by A38, XXREAL_0:2;

then m1 < n1 by XREAL_1:9;

then A69: j + m1 < j + n1 by XREAL_1:8;

A70: ((Q .cut (jj,lP2)) .addEdge e) . m = (Q .cut (jj,lP2)) . m by A31, A45;

(Q .cut (jj,lP2)) . (n1 + 1) = P . (j + n1) by A22, A67;

hence contradiction by A1, A2, A43, A47, A68, A70, A56, A69, A57, Th91; :: thesis: verum

end;reconsider jj = j as odd Element of NAT by ORDINAL1:def 12;

set B = Q .cut (jj,lP2);

len P < (len P) + 2 by XREAL_1:29;

then A19: j <= (len P) + 2 by A15, XXREAL_0:2;

then A20: (Q .cut (jj,lP2)) .last() = x by A9, A6, GLIB_001:37;

A21: (len (Q .cut (jj,lP2))) + j = ((len P) + 2) + 1 by A6, A19, GLIB_001:36;

A22: now :: thesis: for i being even Nat st i < (len (Q .cut (jj,lP2))) - 1 holds

( (Q .cut (jj,lP2)) . (i + 1) = P . (j + i) & j + i in dom P )

set C = (Q .cut (jj,lP2)) .addEdge e;( (Q .cut (jj,lP2)) . (i + 1) = P . (j + i) & j + i in dom P )

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 A23: i < (len (Q .cut (jj,lP2))) - 1 ; :: thesis: ( (Q .cut (jj,lP2)) . (i + 1) = P . (j + i) & j + i in dom P )

j + i < ((len (Q .cut (jj,lP2))) - 1) + j by A23, XREAL_1:8;

then A24: j + i <= ((len P) + 2) - 2 by A21, Th3;

(len (Q .cut (jj,lP2))) - 1 < len (Q .cut (jj,lP2)) by XREAL_1:44;

then A25: i < len (Q .cut (jj,lP2)) by A23, XXREAL_0:2;

A26: i in NAT by ORDINAL1:def 12;

then j + i in dom Q by A6, A19, A25, GLIB_001:36;

then A27: 1 <= j + i by FINSEQ_3:25;

(Q .cut (jj,lP2)) . (i + 1) = Q . (j + i) by A6, A19, A26, A25, GLIB_001:36;

hence ( (Q .cut (jj,lP2)) . (i + 1) = P . (j + i) & j + i in dom P ) by A7, A27, A24, FINSEQ_3:25; :: thesis: verum

end;assume A23: i < (len (Q .cut (jj,lP2))) - 1 ; :: thesis: ( (Q .cut (jj,lP2)) . (i + 1) = P . (j + i) & j + i in dom P )

j + i < ((len (Q .cut (jj,lP2))) - 1) + j by A23, XREAL_1:8;

then A24: j + i <= ((len P) + 2) - 2 by A21, Th3;

(len (Q .cut (jj,lP2))) - 1 < len (Q .cut (jj,lP2)) by XREAL_1:44;

then A25: i < len (Q .cut (jj,lP2)) by A23, XXREAL_0:2;

A26: i in NAT by ORDINAL1:def 12;

then j + i in dom Q by A6, A19, A25, GLIB_001:36;

then A27: 1 <= j + i by FINSEQ_3:25;

(Q .cut (jj,lP2)) . (i + 1) = Q . (j + i) by A6, A19, A26, A25, GLIB_001:36;

hence ( (Q .cut (jj,lP2)) . (i + 1) = P . (j + i) & j + i in dom P ) by A7, A27, A24, FINSEQ_3:25; :: thesis: verum

A28: (Q .cut (jj,lP2)) .first() = Q . j by A6, A19, GLIB_001:37;

A29: (Q .cut (jj,lP2)) .first() = Q . j by A6, A19, GLIB_001:37;

then A30: e Joins (Q .cut (jj,lP2)) .last() ,(Q .cut (jj,lP2)) .first() ,G by A17, A20;

A31: now :: thesis: for n being odd Nat st n <= len (Q .cut (jj,lP2)) holds

((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n

A33:
((len P) + 3) - ((len P) - 2) < ((len P) + 3) - j
by A18, XREAL_1:15;((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n

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 A32: n <= len (Q .cut (jj,lP2)) ; :: thesis: ((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n

1 <= n by Th2;

then n in dom (Q .cut (jj,lP2)) by A32, FINSEQ_3:25;

hence ((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n by A30, GLIB_001:65; :: thesis: verum

end;assume A32: n <= len (Q .cut (jj,lP2)) ; :: thesis: ((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n

1 <= n by Th2;

then n in dom (Q .cut (jj,lP2)) by A32, FINSEQ_3:25;

hence ((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n by A30, GLIB_001:65; :: thesis: verum

then A34: 3 < len (Q .cut (jj,lP2)) by A21, XXREAL_0:2;

(len (Q .cut (jj,lP2))) + 2 > 5 + 2 by A21, A33, XREAL_1:8;

then A35: len ((Q .cut (jj,lP2)) .addEdge e) > 7 by A17, A20, GLIB_000:14, GLIB_001:64;

A36: now :: thesis: not ((Q .cut (jj,lP2)) .addEdge e) .length() <= 3

P .vertexAt j = P . j
by A15, GLIB_001:def 8;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:64;

then (2 * (((Q .cut (jj,lP2)) .addEdge e) .length())) + 1 <= (2 * 3) + 1 by XREAL_1:6;

hence contradiction by A35, GLIB_001:112; :: thesis: verum

end;then 2 * (((Q .cut (jj,lP2)) .addEdge e) .length()) <= 2 * 3 by XREAL_1:64;

then (2 * (((Q .cut (jj,lP2)) .addEdge e) .length())) + 1 <= (2 * 3) + 1 by XREAL_1:6;

hence contradiction by A35, GLIB_001:112; :: thesis: verum

then P . j in P .vertices() by A16, A13, A14, GLIB_001:89, XXREAL_0:2;

then (Q .cut (jj,lP2)) .first() in P .vertices() by A7, A13, A14, A28, XXREAL_0:2;

then A37: Q .cut (jj,lP2) is open by A3, A20;

then (Q .cut (jj,lP2)) .addEdge e is Cycle-like by A17, A34, A29, A20, Th33, GLIB_000:14;

then (Q .cut (jj,lP2)) .addEdge e is chordal by A36, Def11;

then consider m, n being odd Nat such that

A38: m + 2 < n and

A39: n <= len ((Q .cut (jj,lP2)) .addEdge e) and

A40: ((Q .cut (jj,lP2)) .addEdge e) . m <> ((Q .cut (jj,lP2)) .addEdge e) . n and

A41: ex e being object st e Joins ((Q .cut (jj,lP2)) .addEdge e) . m,((Q .cut (jj,lP2)) .addEdge e) . n,G and

A42: ( (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 Th83;

consider e being object such that

A43: e Joins ((Q .cut (jj,lP2)) .addEdge e) . m,((Q .cut (jj,lP2)) .addEdge e) . n,G by A41;

1 <= m by Th2;

then 1 - 1 <= m - 1 by XREAL_1:9;

then reconsider m1 = m - 1 as even Element of NAT by INT_1:3;

reconsider m1 = m1 as even Nat ;

A44: len ((Q .cut (jj,lP2)) .addEdge e) = (len (Q .cut (jj,lP2))) + 2 by A17, A20, GLIB_000:14, GLIB_001:64;

then m + 2 < (len (Q .cut (jj,lP2))) + 2 by A38, A39, XXREAL_0:2;

then A45: (m + 2) - 2 < ((len (Q .cut (jj,lP2))) + 2) - 2 by XREAL_1:9;

then A46: m1 < (len (Q .cut (jj,lP2))) - 1 by XREAL_1:9;

then A47: (Q .cut (jj,lP2)) . (m1 + 1) = P . (j + m1) by A22;

A48: j + m1 in dom P by A22, A46;

then A49: j + m1 <= len P by FINSEQ_3:25;

A50: ((Q .cut (jj,lP2)) .addEdge e) .last() = Q . j by A28, A30, GLIB_001:63;

now :: thesis: not n = len ((Q .cut (jj,lP2)) .addEdge e)

then
n < (len (Q .cut (jj,lP2))) + (2 * 1)
by A44, A39, XXREAL_0:1;assume A51:
n = len ((Q .cut (jj,lP2)) .addEdge e)
; :: thesis: contradiction

then e Joins P . (j + m1),Q . j,G by A31, A50, A43, A45, A47;

then e Joins P . (j + m1),P . j,G by A7, A13, A14, XXREAL_0:2;

then A52: e Joins P . j,P . (j + m1),G ;

3 < m by A17, A34, A29, A20, A37, A42, A51, Th7, Th33, GLIB_000:14, XXREAL_0:2;

then A53: (2 + 1) - 1 < m - 1 by XREAL_1:9;

then A54: j < j + m1 by XREAL_1:29;

j + 2 < j + m1 by A53, XREAL_1:8;

hence contradiction by A1, A2, A49, A52, A54, Th91; :: thesis: verum

end;then e Joins P . (j + m1),Q . j,G by A31, A50, A43, A45, A47;

then e Joins P . (j + m1),P . j,G by A7, A13, A14, XXREAL_0:2;

then A52: e Joins P . j,P . (j + m1),G ;

3 < m by A17, A34, A29, A20, A37, A42, A51, Th7, Th33, GLIB_000:14, XXREAL_0:2;

then A53: (2 + 1) - 1 < m - 1 by XREAL_1:9;

then A54: j < j + m1 by XREAL_1:29;

j + 2 < j + m1 by A53, XREAL_1:8;

hence contradiction by A1, A2, A49, A52, A54, Th91; :: thesis: verum

then A55: n <= ((len (Q .cut (jj,lP2))) + 2) - 2 by Th3;

then A56: ((Q .cut (jj,lP2)) .addEdge e) . n = (Q .cut (jj,lP2)) . n by A31;

1 <= n by Th2;

then 1 - 1 <= n - 1 by XREAL_1:9;

then reconsider n1 = n - 1 as even Element of NAT by INT_1:3;

reconsider n1 = n1 as even Nat ;

(m + 2) - 1 < n - 1 by A38, XREAL_1:9;

then j + (m1 + 2) < j + n1 by XREAL_1:8;

then A57: (j + m1) + 2 < j + n1 ;

now :: thesis: not n = len (Q .cut (jj,lP2))

then
n < len (Q .cut (jj,lP2))
by A55, XXREAL_0:1;
((Q .cut (jj,lP2)) .addEdge e) . m = (Q .cut (jj,lP2)) . m
by A31, A45;

then A58: ((Q .cut (jj,lP2)) .addEdge e) . m = Q . (j + m1) by A7, A47, A49;

A59: len P < (len P) + 2 by XREAL_1:29;

j + m1 <= len P by A48, FINSEQ_3:25;

then consider kk being Nat such that

A60: (j + m1) + (2 * kk) = (len P) + 2 by A59, Lm2, XXREAL_0:2;

assume A61: n = len (Q .cut (jj,lP2)) ; :: thesis: contradiction

then 1 < m by A34, A37, A30, A44, A42, A61, Th33, XXREAL_0:1;

then A63: 1 - 1 < m - 1 by XREAL_1:9;

hence contradiction by A10, A43, A60, A62, A64, A65, A58; :: thesis: verum

end;then A58: ((Q .cut (jj,lP2)) .addEdge e) . m = Q . (j + m1) by A7, A47, A49;

A59: len P < (len P) + 2 by XREAL_1:29;

j + m1 <= len P by A48, FINSEQ_3:25;

then consider kk being Nat such that

A60: (j + m1) + (2 * kk) = (len P) + 2 by A59, Lm2, XXREAL_0:2;

assume A61: n = len (Q .cut (jj,lP2)) ; :: thesis: contradiction

A62: now :: thesis: not 2 * kk < 3 + 1

1 <= m
by Th2;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 A21, A38, A40, A61, A60; :: thesis: verum

end;then 2 * kk <= 3 by NAT_1:13;

then ( 2 * kk = 0 or 2 * kk = 2 ) by Th11;

hence contradiction by A21, A38, A40, A61, A60; :: thesis: verum

then 1 < m by A34, A37, A30, A44, A42, A61, Th33, XXREAL_0:1;

then A63: 1 - 1 < m - 1 by XREAL_1:9;

A64: now :: thesis: not 2 * kk > (len P) + 1

assume
2 * kk > (len P) + 1
; :: thesis: contradiction

then 2 * kk >= ((len P) + 1) + 1 by NAT_1:13;

hence contradiction by A60, XREAL_1:29; :: thesis: verum

end;then 2 * kk >= ((len P) + 1) + 1 by NAT_1:13;

hence contradiction by A60, XREAL_1:29; :: thesis: verum

A65: now :: thesis: not kk >= k

((Q .cut (jj,lP2)) .addEdge e) . n = x
by A20, A31, A61;assume
kk >= k
; :: thesis: contradiction

then A66: 2 * kk >= 2 * k by XREAL_1:64;

(j + (2 * kk)) + m1 > j + (2 * kk) by A63, XREAL_1:29;

hence contradiction by A12, A60, A66, XREAL_1:7; :: thesis: verum

end;then A66: 2 * kk >= 2 * k by XREAL_1:64;

(j + (2 * kk)) + m1 > j + (2 * kk) by A63, XREAL_1:29;

hence contradiction by A12, A60, A66, XREAL_1:7; :: thesis: verum

hence contradiction by A10, A43, A60, A62, A64, A65, A58; :: thesis: verum

then A67: n1 < (len (Q .cut (jj,lP2))) - 1 by XREAL_1:9;

then j + n1 in dom P by A22;

then A68: j + n1 <= len P by FINSEQ_3:25;

m < m + 2 by XREAL_1:29;

then m < n by A38, XXREAL_0:2;

then m1 < n1 by XREAL_1:9;

then A69: j + m1 < j + n1 by XREAL_1:8;

A70: ((Q .cut (jj,lP2)) .addEdge e) . m = (Q .cut (jj,lP2)) . m by A31, A45;

(Q .cut (jj,lP2)) . (n1 + 1) = P . (j + n1) by A22, A67;

hence contradiction by A1, A2, A43, A47, A68, A70, A56, A69, A57, Th91; :: thesis: verum

S

S

A72: for k being Nat holds S

A73: now :: thesis: for n being odd Nat st n <= (len P) - 2 holds

for e being object holds not e Joins Q . n,x,G

for e being object holds not e Joins Q . n,x,G

let n be odd Nat; :: thesis: ( n <= (len P) - 2 implies for e being object holds not e Joins Q . n,x,G )

assume A74: n <= (len P) - 2 ; :: thesis: for e being object holds not e Joins Q . n,x,G

(len P) - 2 <= ((len P) - 2) + 4 by XREAL_1:31;

then consider k being Nat such that

A75: n + (2 * k) = (len P) + 2 by A74, Lm2, XXREAL_0:2;

end;assume A74: n <= (len P) - 2 ; :: thesis: for e being object holds not e Joins Q . n,x,G

(len P) - 2 <= ((len P) - 2) + 4 by XREAL_1:31;

then consider k being Nat such that

A75: n + (2 * k) = (len P) + 2 by A74, Lm2, XXREAL_0:2;

A76: now :: thesis: not 2 * k > (len P) + 1

assume
2 * k > (len P) + 1
; :: thesis: contradiction

then n + (2 * k) > 1 + ((len P) + 1) by Th2, XREAL_1:8;

hence contradiction by A75; :: thesis: verum

end;then n + (2 * k) > 1 + ((len P) + 1) by Th2, XREAL_1:8;

hence contradiction by A75; :: thesis: verum

now :: thesis: not 2 * k < 4

hence
for e being object holds not e Joins Q . n,x,G
by A72, A75, A76; :: thesis: verumassume A77:
2 * k < 4
; :: thesis: contradiction

n + 4 <= ((len P) - 2) + 4 by A74, XREAL_1:7;

hence contradiction by A75, A77, XREAL_1:8; :: thesis: verum

end;n + 4 <= ((len P) - 2) + 4 by A74, XREAL_1:7;

hence contradiction by A75, A77, XREAL_1:8; :: thesis: verum

A78: now :: thesis: not Q is chordal

Q .first() = P .first()
by A4, GLIB_001:63;assume
Q is chordal
; :: thesis: contradiction

then consider m, n being odd Nat such that

A79: m + 2 < n and

A80: n <= len Q and

Q . m <> Q . n and

A81: ex e being object 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 Th83;

m + 2 < (len P) + 2 by A6, A79, A80, XXREAL_0:2;

then A82: (m + 2) - 2 < ((len P) + 2) - 2 by XREAL_1:9;

m < m + 2 by XREAL_1:29;

then A83: m < n by A79, XXREAL_0:2;

end;then consider m, n being odd Nat such that

A79: m + 2 < n and

A80: n <= len Q and

Q . m <> Q . n and

A81: ex e being object 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 Th83;

m + 2 < (len P) + 2 by A6, A79, A80, XXREAL_0:2;

then A82: (m + 2) - 2 < ((len P) + 2) - 2 by XREAL_1:9;

m < m + 2 by XREAL_1:29;

then A83: m < n by A79, XXREAL_0:2;

then Q .first() in P .vertices() by GLIB_001:88;

hence ( P .addEdge e is Path-like & P .addEdge e is open & P .addEdge e is chordless ) by A3, A9, A78; :: thesis: verum