let G be finite chordal _Graph; :: thesis: for a, b being Vertex of G st a <> b & not a,b are_adjacent holds

for S being VertexSeparator of a,b st S is minimal holds

for H being removeVertices of G,S

for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) )

let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b st S is minimal holds

for H being removeVertices of G,S

for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) ) )

assume that

A1: a <> b and

A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b st S is minimal holds

for H being removeVertices of G,S

for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) )

let S be VertexSeparator of a,b; :: thesis: ( S is minimal implies for H being removeVertices of G,S

for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) ) )

assume A3: S is minimal ; :: thesis: for H being removeVertices of G,S

for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) )

let H be removeVertices of G,S; :: thesis: for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) )

let a1 be Vertex of H; :: thesis: ( a = a1 implies ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) ) )

assume A4: a = a1 ; :: thesis: ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) )

assume A5: for c being Vertex of G holds

( not c in H .reachableFrom a1 or ex x being Vertex of G st

( x in S & not c,x are_adjacent ) ) ; :: thesis: contradiction

for S being VertexSeparator of a,b st S is minimal holds

for H being removeVertices of G,S

for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) )

let a, b be Vertex of G; :: thesis: ( a <> b & not a,b are_adjacent implies for S being VertexSeparator of a,b st S is minimal holds

for H being removeVertices of G,S

for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) ) )

assume that

A1: a <> b and

A2: not a,b are_adjacent ; :: thesis: for S being VertexSeparator of a,b st S is minimal holds

for H being removeVertices of G,S

for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) )

let S be VertexSeparator of a,b; :: thesis: ( S is minimal implies for H being removeVertices of G,S

for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) ) )

assume A3: S is minimal ; :: thesis: for H being removeVertices of G,S

for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) )

let H be removeVertices of G,S; :: thesis: for a1 being Vertex of H st a = a1 holds

ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) )

let a1 be Vertex of H; :: thesis: ( a = a1 implies ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) ) )

assume A4: a = a1 ; :: thesis: ex c being Vertex of G st

( c in H .reachableFrom a1 & ( for x being Vertex of G st x in S holds

c,x are_adjacent ) )

assume A5: for c being Vertex of G holds

( not c in H .reachableFrom a1 or ex x being Vertex of G st

( x in S & not c,x are_adjacent ) ) ; :: thesis: contradiction

per cases
( S is empty or not S is empty )
;

end;

suppose
S is empty
; :: thesis: contradiction

then
for x being Vertex of G holds

( not x in S or a,x are_adjacent ) ;

hence contradiction by A4, A5, GLIB_002:9; :: thesis: verum

end;( not x in S or a,x are_adjacent ) ;

hence contradiction by A4, A5, GLIB_002:9; :: thesis: verum

suppose
not S is empty
; :: thesis: contradiction

then reconsider S = S as non empty Subset of (the_Vertices_of G) ;

set A = H .reachableFrom a1;

deffunc H_{1}( set ) -> Element of omega = card ((G .AdjacentSet {$1}) /\ S);

set M = { H_{1}(x) where x is Vertex of G : x in H .reachableFrom a1 } ;

A8: { H_{1}(x) where x is Vertex of G : x in H .reachableFrom a1 } is finite
from FRAENKEL:sch 21(A7);

a in H .reachableFrom a1 by A4, GLIB_002:9;

then card ((G .AdjacentSet {a}) /\ S) in { H_{1}(x) where x is Vertex of G : x in H .reachableFrom a1 }
;

then reconsider M = { H_{1}(x) where x is Vertex of G : x in H .reachableFrom a1 } as non empty finite natural-membered set by A8, A6, MEMBERED:def 6;

set Ga = the inducedSubgraph of H,(H .reachableFrom a1);

A9: the_Vertices_of the inducedSubgraph of H,(H .reachableFrom a1) = H .reachableFrom a1 by GLIB_000:def 37;

max M in M by XXREAL_2:def 8;

then consider c being Vertex of G such that

A10: max M = card ((G .AdjacentSet {c}) /\ S) and

A11: c in H .reachableFrom a1 ;

set gcs = (G .AdjacentSet {c}) /\ S;

A12: (H .reachableFrom a1) /\ S = {} by A1, A2, Th74;

set Gs = the inducedSubgraph of G,S;

set tVG = the_Vertices_of G;

A13: (2 * 0) + 1 is odd ;

not a in S by A1, A2, Def8;

then A14: (the_Vertices_of G) \ S is non empty Subset of (the_Vertices_of G) by XBOOLE_0:def 5;

the_Vertices_of H c= the_Vertices_of G ;

then reconsider A = H .reachableFrom a1 as non empty Subset of (the_Vertices_of G) by XBOOLE_1:1;

then reconsider Ga = the inducedSubgraph of H,(H .reachableFrom a1) as inducedSubgraph of G,A by A14, Th29;

consider y being Vertex of G such that

A16: y in S and

A17: not c,y are_adjacent by A5, A11;

A18: not y in A by A16, A12, XBOOLE_0:def 4;

set Ay = A \/ {y};

set Gay = the inducedSubgraph of G,(A \/ {y});

y in {y} by TARSKI:def 1;

then A19: y in A \/ {y} by XBOOLE_0:def 3;

c in A \/ {y} by A11, XBOOLE_0:def 3;

then reconsider ca = c, ya = y as Vertex of the inducedSubgraph of G,(A \/ {y}) by A19, GLIB_000:def 37;

ex yaa being Vertex of G st

( yaa in A & y,yaa are_adjacent ) by A1, A2, A3, A4, A16, Th81;

then y in G .AdjacentSet (the_Vertices_of Ga) by A9, A18;

then the inducedSubgraph of G,(A \/ {y}) is connected by Th56;

then consider Wa being Walk of the inducedSubgraph of G,(A \/ {y}) such that

A20: Wa is_Walk_from ca,ya ;

consider P being Path of the inducedSubgraph of G,(A \/ {y}) such that

A21: P is_Walk_from Wa .first() ,Wa .last() and

A22: P is minlength by Th38;

Wa .first() = ca by A20;

then A23: P .first() = ca by A21;

Wa .last() = ya by A20;

then A24: P .last() = y by A21;

c <> y by A11, A16, A12, XBOOLE_0:def 4;

then not P is trivial by A23, A24, GLIB_001:127;

then A25: len P >= 3 by GLIB_001:125;

then reconsider j = (len P) - (2 * 1) as odd Element of NAT by INT_1:3, XXREAL_0:2;

set d = P . j;

A28: j < len P by XREAL_1:44;

A31: the_Vertices_of the inducedSubgraph of G,(A \/ {y}) = A \/ {y} by GLIB_000:def 37;

A32: P . j in the_Vertices_of the inducedSubgraph of G,(A \/ {y}) by A28, GLIB_001:7;

then A33: ( P . j in A or P . j in {y} ) by A31, XBOOLE_0:def 3;

reconsider d = P . j as Vertex of G by A32;

set gds = (G .AdjacentSet {d}) /\ S;

P . (j + 1) Joins d,P . (((len P) - 2) + 2), the inducedSubgraph of G,(A \/ {y}) by A28, GLIB_001:def 3;

then A34: P . (j + 1) Joins d,y,G by A24, GLIB_000:72;

then d,y are_adjacent ;

then A35: y in G .AdjacentSet {d} by A29, Th51;

then A36: y in (G .AdjacentSet {d}) /\ S by A16, XBOOLE_0:def 4;

A39: x in (G .AdjacentSet {c}) /\ S and

A40: not x in (G .AdjacentSet {d}) /\ S ;

A41: x in S by A39, XBOOLE_0:def 4;

then A42: not x in G .AdjacentSet {d} by A40, XBOOLE_0:def 4;

reconsider x = x as Vertex of G by A39;

defpred S_{1}[ Nat] means ( $1 in dom P & $1 is odd & $1 < len P & ex e being object st e Joins x,P . $1,G );

A43: for k being Nat st S_{1}[k] holds

k <= len P ;

A44: not x in A by A12, A41, XBOOLE_0:def 4;

A45: 1 < len P by A26, XXREAL_0:2;

then A46: 1 in dom P by FINSEQ_3:25;

x in G .AdjacentSet {c} by A39, XBOOLE_0:def 4;

then c,x are_adjacent by Th51;

then ex e being object st e Joins x,P . 1,G by A23, Def3;

then A47: ex k being Nat st S_{1}[k]
by A45, A46, A13;

consider k being Nat such that

A48: S_{1}[k]
and

A49: for i being Nat st S_{1}[i] holds

k >= i from NAT_1:sch 6(A43, A47);

reconsider k = k as odd Element of NAT by A48;

set Q1 = P .cut (k,j);

reconsider Q = P .cut (k,j) as Path of G by GLIB_001:175;

A50: k <= j by A48, Th3;

A51: j < len P by XREAL_1:44;

then A52: P .cut (k,j) is minlength by A22, A50, Th41;

A53: (len Q) + k = j + 1 by A50, A51, GLIB_001:36;

set dd = Q .last() ;

A64: (P .cut (k,j)) .first() = P . k by A50, A51, GLIB_001:37;

then A65: x,Q .first() are_adjacent by A48;

A66: x <> y by A16, A35, A40, XBOOLE_0:def 4;

then A67: not x in {y} by TARSKI:def 1;

reconsider xs = x, ys = y as Vertex of the inducedSubgraph of G,S by A16, A41, GLIB_000:def 37;

the inducedSubgraph of G,S is complete by A1, A2, A3, Th97;

then xs,ys are_adjacent by A66;

then consider ej being object such that

A68: ej Joins xs,ys, the inducedSubgraph of G,S ;

ej Joins x,y,G by A68, GLIB_000:72;

then A69: x,y are_adjacent ;

A70: (P .cut (k,j)) .last() = P . j by A50, A51, GLIB_001:37;

then A71: Q .last() = P . j ;

d <> x by A12, A33, A29, A41, TARSKI:def 1, XBOOLE_0:def 4;

then A72: not d,x are_adjacent by A42, Th51;

then A73: Q .first() <> Q .last() by A48, A64, A70, Def3;

then A74: Q is open ;

A75: Q .vertices() = (P .cut (k,j)) .vertices() by GLIB_001:98;

then Q .last() in (P .cut (k,j)) .vertices() by GLIB_001:88;

then A76: Q .last() <> x by A31, A44, A67, XBOOLE_0:def 3;

then A93: Q .first() <> x by A31, A44, A67, XBOOLE_0:def 3;

Q .last() ,y are_adjacent by A34, A70;

then consider R being Path of G such that

A94: len R = 7 and

A95: R .length() = 3 and

A96: R .vertices() = {(Q .last()),y,x,(Q .first())} and

A97: R . 1 = Q .last() and

A98: R . 3 = y and

A99: R . 5 = x and

A100: R . 7 = Q .first() by A24, A29, A66, A69, A77, A64, A70, A76, A93, A65, Th47;

A101: not R is trivial by A94, GLIB_001:126;

A102: Q .edges() misses R .edges()

then A119: (Q .vertices()) /\ (R .vertices()) = {(Q .first()),(Q .last())} by A116;

P . k <> P . j by A72, A48, Def3;

then A134: not Q is trivial by A133, A71, GLIB_001:127;

then Q .length() <> 0 ;

then A135: Q .length() >= 0 + 1 by NAT_1:13;

set C = Q .append R;

A136: R .first() = Q .last() by A97;

then A137: (Q .append R) . ((len Q) + 6) = R . (6 + 1) by A94, GLIB_001:33;

A138: (Q .append R) . ((len Q) + 4) = R . (4 + 1) by A94, A136, GLIB_001:33;

A139: (Q .append R) . ((len Q) + 2) = R . (2 + 1) by A94, A136, GLIB_001:33;

(Q .append R) .length() = (Q .length()) + 3 by A95, A136, Th28;

then (Q .append R) .length() >= 1 + 3 by A135, XREAL_1:7;

then A140: (Q .append R) .length() > 3 by NAT_1:13;

A141: R .last() = Q .first() by A94, A100;

then A142: R is open by A73, A136;

then Q .append R is Cycle-like by A74, A136, A141, A101, A102, A119, Th27;

then Q .append R is chordal by A140, Def11;

then consider m, n being odd Nat such that

A143: m + 2 < n and

A144: n <= len (Q .append R) and

(Q .append R) . m <> (Q .append R) . n and

A145: ex e being object st e Joins (Q .append R) . m,(Q .append R) . n,G and

A146: ( Q .append R is Cycle-like implies ( ( not m = 1 or not n = len (Q .append R) ) & ( not m = 1 or not n = (len (Q .append R)) - 2 ) & ( not m = 3 or not n = len (Q .append R) ) ) ) by Th83;

consider e being object such that

A147: e Joins (Q .append R) . m,(Q .append R) . n,G by A145;

A148: ((len (Q .append R)) + 1) + (- 1) = ((len Q) + (len R)) + (- 1) by A136, GLIB_001:28;

A149: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )

end;set A = H .reachableFrom a1;

deffunc H

set M = { H

A6: now :: thesis: for x being object st x in { H_{1}(x) where x is Vertex of G : x in H .reachableFrom a1 } holds

x is natural

A7:
H .reachableFrom a1 is finite
;x is natural

let x be object ; :: thesis: ( x in { H_{1}(x) where x is Vertex of G : x in H .reachableFrom a1 } implies x is natural )

assume x in { H_{1}(x) where x is Vertex of G : x in H .reachableFrom a1 }
; :: thesis: x is natural

then ex y being Vertex of G st

( x = card ((G .AdjacentSet {y}) /\ S) & y in H .reachableFrom a1 ) ;

hence x is natural ; :: thesis: verum

end;assume x in { H

then ex y being Vertex of G st

( x = card ((G .AdjacentSet {y}) /\ S) & y in H .reachableFrom a1 ) ;

hence x is natural ; :: thesis: verum

A8: { H

a in H .reachableFrom a1 by A4, GLIB_002:9;

then card ((G .AdjacentSet {a}) /\ S) in { H

then reconsider M = { H

set Ga = the inducedSubgraph of H,(H .reachableFrom a1);

A9: the_Vertices_of the inducedSubgraph of H,(H .reachableFrom a1) = H .reachableFrom a1 by GLIB_000:def 37;

max M in M by XXREAL_2:def 8;

then consider c being Vertex of G such that

A10: max M = card ((G .AdjacentSet {c}) /\ S) and

A11: c in H .reachableFrom a1 ;

set gcs = (G .AdjacentSet {c}) /\ S;

A12: (H .reachableFrom a1) /\ S = {} by A1, A2, Th74;

set Gs = the inducedSubgraph of G,S;

set tVG = the_Vertices_of G;

A13: (2 * 0) + 1 is odd ;

not a in S by A1, A2, Def8;

then A14: (the_Vertices_of G) \ S is non empty Subset of (the_Vertices_of G) by XBOOLE_0:def 5;

the_Vertices_of H c= the_Vertices_of G ;

then reconsider A = H .reachableFrom a1 as non empty Subset of (the_Vertices_of G) by XBOOLE_1:1;

now :: thesis: for x being object st x in A holds

x in (the_Vertices_of G) \ S

then
A c= (the_Vertices_of G) \ S
;x in (the_Vertices_of G) \ S

let x be object ; :: thesis: ( x in A implies x in (the_Vertices_of G) \ S )

assume A15: x in A ; :: thesis: x in (the_Vertices_of G) \ S

not x in S by A12, A15, XBOOLE_0:def 4;

hence x in (the_Vertices_of G) \ S by A15, XBOOLE_0:def 5; :: thesis: verum

end;assume A15: x in A ; :: thesis: x in (the_Vertices_of G) \ S

not x in S by A12, A15, XBOOLE_0:def 4;

hence x in (the_Vertices_of G) \ S by A15, XBOOLE_0:def 5; :: thesis: verum

then reconsider Ga = the inducedSubgraph of H,(H .reachableFrom a1) as inducedSubgraph of G,A by A14, Th29;

consider y being Vertex of G such that

A16: y in S and

A17: not c,y are_adjacent by A5, A11;

A18: not y in A by A16, A12, XBOOLE_0:def 4;

set Ay = A \/ {y};

set Gay = the inducedSubgraph of G,(A \/ {y});

y in {y} by TARSKI:def 1;

then A19: y in A \/ {y} by XBOOLE_0:def 3;

c in A \/ {y} by A11, XBOOLE_0:def 3;

then reconsider ca = c, ya = y as Vertex of the inducedSubgraph of G,(A \/ {y}) by A19, GLIB_000:def 37;

ex yaa being Vertex of G st

( yaa in A & y,yaa are_adjacent ) by A1, A2, A3, A4, A16, Th81;

then y in G .AdjacentSet (the_Vertices_of Ga) by A9, A18;

then the inducedSubgraph of G,(A \/ {y}) is connected by Th56;

then consider Wa being Walk of the inducedSubgraph of G,(A \/ {y}) such that

A20: Wa is_Walk_from ca,ya ;

consider P being Path of the inducedSubgraph of G,(A \/ {y}) such that

A21: P is_Walk_from Wa .first() ,Wa .last() and

A22: P is minlength by Th38;

Wa .first() = ca by A20;

then A23: P .first() = ca by A21;

Wa .last() = ya by A20;

then A24: P .last() = y by A21;

c <> y by A11, A16, A12, XBOOLE_0:def 4;

then not P is trivial by A23, A24, GLIB_001:127;

then A25: len P >= 3 by GLIB_001:125;

A26: now :: thesis: not len P < (2 * 2) + 1

then
5 + (- 2) <= (len P) + (- 2)
by XREAL_1:7;assume
len P < (2 * 2) + 1
; :: thesis: contradiction

then len P <= 5 - 2 by Th3;

then A27: len P = 3 by A25, XXREAL_0:1;

then (2 * 0) + 1 < len P ;

then P . (1 + 1) Joins P . 1,P . (1 + 2), the inducedSubgraph of G,(A \/ {y}) by GLIB_001:def 3;

then P . 2 Joins c,y,G by A23, A24, A27, GLIB_000:72;

hence contradiction by A17; :: thesis: verum

end;then len P <= 5 - 2 by Th3;

then A27: len P = 3 by A25, XXREAL_0:1;

then (2 * 0) + 1 < len P ;

then P . (1 + 1) Joins P . 1,P . (1 + 2), the inducedSubgraph of G,(A \/ {y}) by GLIB_001:def 3;

then P . 2 Joins c,y,G by A23, A24, A27, GLIB_000:72;

hence contradiction by A17; :: thesis: verum

then reconsider j = (len P) - (2 * 1) as odd Element of NAT by INT_1:3, XXREAL_0:2;

set d = P . j;

A28: j < len P by XREAL_1:44;

A29: now :: thesis: not P . j = y

A30:
not y in G .AdjacentSet {c}
by A17, Th51;assume
P . j = y
; :: thesis: contradiction

then (len P) - 2 = 1 by A24, A28, GLIB_001:def 28;

then len P = 1 + 2 ;

hence contradiction by A26; :: thesis: verum

end;then (len P) - 2 = 1 by A24, A28, GLIB_001:def 28;

then len P = 1 + 2 ;

hence contradiction by A26; :: thesis: verum

A31: the_Vertices_of the inducedSubgraph of G,(A \/ {y}) = A \/ {y} by GLIB_000:def 37;

A32: P . j in the_Vertices_of the inducedSubgraph of G,(A \/ {y}) by A28, GLIB_001:7;

then A33: ( P . j in A or P . j in {y} ) by A31, XBOOLE_0:def 3;

reconsider d = P . j as Vertex of G by A32;

set gds = (G .AdjacentSet {d}) /\ S;

P . (j + 1) Joins d,P . (((len P) - 2) + 2), the inducedSubgraph of G,(A \/ {y}) by A28, GLIB_001:def 3;

then A34: P . (j + 1) Joins d,y,G by A24, GLIB_000:72;

then d,y are_adjacent ;

then A35: y in G .AdjacentSet {d} by A29, Th51;

then A36: y in (G .AdjacentSet {d}) /\ S by A16, XBOOLE_0:def 4;

now :: thesis: not (G .AdjacentSet {c}) /\ S c= (G .AdjacentSet {d}) /\ S

then consider x being object such that assume A37:
(G .AdjacentSet {c}) /\ S c= (G .AdjacentSet {d}) /\ S
; :: thesis: contradiction

not y in (G .AdjacentSet {c}) /\ S by A30, XBOOLE_0:def 4;

then (G .AdjacentSet {c}) /\ S c< (G .AdjacentSet {d}) /\ S by A36, A37;

then A38: card ((G .AdjacentSet {c}) /\ S) < card ((G .AdjacentSet {d}) /\ S) by TREES_1:6;

card ((G .AdjacentSet {d}) /\ S) in M by A33, A29, TARSKI:def 1;

hence contradiction by A10, A38, XXREAL_2:def 8; :: thesis: verum

end;not y in (G .AdjacentSet {c}) /\ S by A30, XBOOLE_0:def 4;

then (G .AdjacentSet {c}) /\ S c< (G .AdjacentSet {d}) /\ S by A36, A37;

then A38: card ((G .AdjacentSet {c}) /\ S) < card ((G .AdjacentSet {d}) /\ S) by TREES_1:6;

card ((G .AdjacentSet {d}) /\ S) in M by A33, A29, TARSKI:def 1;

hence contradiction by A10, A38, XXREAL_2:def 8; :: thesis: verum

A39: x in (G .AdjacentSet {c}) /\ S and

A40: not x in (G .AdjacentSet {d}) /\ S ;

A41: x in S by A39, XBOOLE_0:def 4;

then A42: not x in G .AdjacentSet {d} by A40, XBOOLE_0:def 4;

reconsider x = x as Vertex of G by A39;

defpred S

A43: for k being Nat st S

k <= len P ;

A44: not x in A by A12, A41, XBOOLE_0:def 4;

A45: 1 < len P by A26, XXREAL_0:2;

then A46: 1 in dom P by FINSEQ_3:25;

x in G .AdjacentSet {c} by A39, XBOOLE_0:def 4;

then c,x are_adjacent by Th51;

then ex e being object st e Joins x,P . 1,G by A23, Def3;

then A47: ex k being Nat st S

consider k being Nat such that

A48: S

A49: for i being Nat st S

k >= i from NAT_1:sch 6(A43, A47);

reconsider k = k as odd Element of NAT by A48;

set Q1 = P .cut (k,j);

reconsider Q = P .cut (k,j) as Path of G by GLIB_001:175;

A50: k <= j by A48, Th3;

A51: j < len P by XREAL_1:44;

then A52: P .cut (k,j) is minlength by A22, A50, Th41;

A53: (len Q) + k = j + 1 by A50, A51, GLIB_001:36;

A54: now :: thesis: for i being odd Nat st i in dom Q & i <> 1 holds

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

set cc = Q .first() ;for e being object holds not e Joins Q . i,x,G

let i be odd Nat; :: thesis: ( i in dom Q & i <> 1 implies for e being object holds not e Joins Q . i,x,G )

assume that

A55: i in dom Q and

A56: i <> 1 ; :: thesis: for e being object holds not e Joins Q . i,x,G

1 <= i by A55, FINSEQ_3:25;

then 1 + (- 1) <= i + (- 1) by XREAL_1:7;

then reconsider i1 = i - 1 as even Element of NAT by INT_1:3;

reconsider ki1 = k + i1 as odd Element of NAT ;

A57: i + (- 1) < i + (- 0) by XREAL_1:8;

i <= len Q by A55, FINSEQ_3:25;

then A58: i1 < len Q by A57, XXREAL_0:2;

then A59: ki1 in dom P by A50, A51, GLIB_001:36;

A60: (len P) + (- 1) < (len P) + (- 0) by XREAL_1:8;

assume A61: ex e being object st e Joins Q . i,x,G ; :: thesis: contradiction

i1 + k < (((len P) - 1) - k) + k by A53, A58, XREAL_1:8;

then A62: ki1 < len P by A60, XXREAL_0:2;

A63: Q . (i1 + 1) = P . ki1 by A50, A51, A58, GLIB_001:36;

end;assume that

A55: i in dom Q and

A56: i <> 1 ; :: thesis: for e being object holds not e Joins Q . i,x,G

1 <= i by A55, FINSEQ_3:25;

then 1 + (- 1) <= i + (- 1) by XREAL_1:7;

then reconsider i1 = i - 1 as even Element of NAT by INT_1:3;

reconsider ki1 = k + i1 as odd Element of NAT ;

A57: i + (- 1) < i + (- 0) by XREAL_1:8;

i <= len Q by A55, FINSEQ_3:25;

then A58: i1 < len Q by A57, XXREAL_0:2;

then A59: ki1 in dom P by A50, A51, GLIB_001:36;

A60: (len P) + (- 1) < (len P) + (- 0) by XREAL_1:8;

assume A61: ex e being object st e Joins Q . i,x,G ; :: thesis: contradiction

i1 + k < (((len P) - 1) - k) + k by A53, A58, XREAL_1:8;

then A62: ki1 < len P by A60, XXREAL_0:2;

A63: Q . (i1 + 1) = P . ki1 by A50, A51, A58, GLIB_001:36;

now :: thesis: not i1 <> 0

hence
contradiction
by A56; :: thesis: verumassume
i1 <> 0
; :: thesis: contradiction

then k + 0 < k + i1 by XREAL_1:8;

hence contradiction by A49, A61, A63, A59, A62, GLIB_000:14; :: thesis: verum

end;then k + 0 < k + i1 by XREAL_1:8;

hence contradiction by A49, A61, A63, A59, A62, GLIB_000:14; :: thesis: verum

set dd = Q .last() ;

A64: (P .cut (k,j)) .first() = P . k by A50, A51, GLIB_001:37;

then A65: x,Q .first() are_adjacent by A48;

A66: x <> y by A16, A35, A40, XBOOLE_0:def 4;

then A67: not x in {y} by TARSKI:def 1;

reconsider xs = x, ys = y as Vertex of the inducedSubgraph of G,S by A16, A41, GLIB_000:def 37;

the inducedSubgraph of G,S is complete by A1, A2, A3, Th97;

then xs,ys are_adjacent by A66;

then consider ej being object such that

A68: ej Joins xs,ys, the inducedSubgraph of G,S ;

ej Joins x,y,G by A68, GLIB_000:72;

then A69: x,y are_adjacent ;

A70: (P .cut (k,j)) .last() = P . j by A50, A51, GLIB_001:37;

then A71: Q .last() = P . j ;

d <> x by A12, A33, A29, A41, TARSKI:def 1, XBOOLE_0:def 4;

then A72: not d,x are_adjacent by A42, Th51;

then A73: Q .first() <> Q .last() by A48, A64, A70, Def3;

then A74: Q is open ;

A75: Q .vertices() = (P .cut (k,j)) .vertices() by GLIB_001:98;

then Q .last() in (P .cut (k,j)) .vertices() by GLIB_001:88;

then A76: Q .last() <> x by A31, A44, A67, XBOOLE_0:def 3;

A77: now :: thesis: not P . k = P . (len P)

A78:
(2 * 0) + 1 <= k
by ABIAN:12;

then A79: (len (P .cut (1,k))) + 1 = k + 1 by A48, GLIB_001:36;

assume P . k = P . (len P) ; :: thesis: contradiction

then P .cut (1,k) is_Walk_from P .first() ,P .last() by A48, A78, GLIB_001:37;

hence contradiction by A22, A48, A79; :: thesis: verum

end;then A79: (len (P .cut (1,k))) + 1 = k + 1 by A48, GLIB_001:36;

assume P . k = P . (len P) ; :: thesis: contradiction

then P .cut (1,k) is_Walk_from P .first() ,P .last() by A48, A78, GLIB_001:37;

hence contradiction by A22, A48, A79; :: thesis: verum

A80: now :: thesis: for v being set st v in Q .vertices() holds

v in A

Q .first() in (P .cut (k,j)) .vertices()
by A75, GLIB_001:88;v in A

let v be set ; :: thesis: ( v in Q .vertices() implies v in A )

assume A81: v in Q .vertices() ; :: thesis: v in A

consider n being odd Element of NAT such that

A82: n <= len Q and

A83: Q . n = v by A81, GLIB_001:87;

1 <= n by ABIAN:12;

then 1 + (- 1) <= n + (- 1) by XREAL_1:7;

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

reconsider kn1 = k + n1 as odd Element of NAT ;

A84: (len P) + (- 1) < (len P) + (- 0) by XREAL_1:8;

n + (- 1) < n + (- 0) by XREAL_1:8;

then A85: n1 < len Q by A82, XXREAL_0:2;

then k + n1 < (((len P) - 1) - k) + k by A53, XREAL_1:8;

then A86: kn1 < len P by A84, XXREAL_0:2;

A87: Q . (n1 + 1) = P . kn1 by A50, A51, A85, GLIB_001:36;

Q .vertices() c= P .vertices() by A50, A51, A75, GLIB_001:94;

then v in P .vertices() by A81;

hence v in A by A31, A92, XBOOLE_0:def 3; :: thesis: verum

end;assume A81: v in Q .vertices() ; :: thesis: v in A

consider n being odd Element of NAT such that

A82: n <= len Q and

A83: Q . n = v by A81, GLIB_001:87;

1 <= n by ABIAN:12;

then 1 + (- 1) <= n + (- 1) by XREAL_1:7;

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

reconsider kn1 = k + n1 as odd Element of NAT ;

A84: (len P) + (- 1) < (len P) + (- 0) by XREAL_1:8;

n + (- 1) < n + (- 0) by XREAL_1:8;

then A85: n1 < len Q by A82, XXREAL_0:2;

then k + n1 < (((len P) - 1) - k) + k by A53, XREAL_1:8;

then A86: kn1 < len P by A84, XXREAL_0:2;

A87: Q . (n1 + 1) = P . kn1 by A50, A51, A85, GLIB_001:36;

now :: thesis: not v = y

then A92:
not v in {y}
by TARSKI:def 1;A88:
1 <= k
by ABIAN:12;

assume A89: v = y ; :: thesis: contradiction

then A90: k + (n + (- 1)) = 1 by A24, A83, A87, A86, GLIB_001:def 28;

hence contradiction by A24, A77, A64, A83, A89, A91, XXREAL_0:1; :: thesis: verum

end;assume A89: v = y ; :: thesis: contradiction

then A90: k + (n + (- 1)) = 1 by A24, A83, A87, A86, GLIB_001:def 28;

A91: now :: thesis: not 1 < n

1 <= n
by ABIAN:12;assume
1 < n
; :: thesis: contradiction

then 1 + 1 <= n by NAT_1:13;

then 2 + 1 <= k + n by A88, XREAL_1:7;

hence contradiction by A90; :: thesis: verum

end;then 1 + 1 <= n by NAT_1:13;

then 2 + 1 <= k + n by A88, XREAL_1:7;

hence contradiction by A90; :: thesis: verum

hence contradiction by A24, A77, A64, A83, A89, A91, XXREAL_0:1; :: thesis: verum

Q .vertices() c= P .vertices() by A50, A51, A75, GLIB_001:94;

then v in P .vertices() by A81;

hence v in A by A31, A92, XBOOLE_0:def 3; :: thesis: verum

then A93: Q .first() <> x by A31, A44, A67, XBOOLE_0:def 3;

Q .last() ,y are_adjacent by A34, A70;

then consider R being Path of G such that

A94: len R = 7 and

A95: R .length() = 3 and

A96: R .vertices() = {(Q .last()),y,x,(Q .first())} and

A97: R . 1 = Q .last() and

A98: R . 3 = y and

A99: R . 5 = x and

A100: R . 7 = Q .first() by A24, A29, A66, A69, A77, A64, A70, A76, A93, A65, Th47;

A101: not R is trivial by A94, GLIB_001:126;

A102: Q .edges() misses R .edges()

proof

assume
not Q .edges() misses R .edges()
; :: thesis: contradiction

then (Q .edges()) /\ (R .edges()) <> {} ;

then consider e being object such that

A103: e in (Q .edges()) /\ (R .edges()) by XBOOLE_0:def 1;

A104: e in Q .edges() by A103, XBOOLE_0:def 4;

e in R .edges() by A103, XBOOLE_0:def 4;

then consider n being even Element of NAT such that

A105: 1 <= n and

A106: n <= 7 and

A107: R . n = e by A94, GLIB_001:99;

end;then (Q .edges()) /\ (R .edges()) <> {} ;

then consider e being object such that

A103: e in (Q .edges()) /\ (R .edges()) by XBOOLE_0:def 1;

A104: e in Q .edges() by A103, XBOOLE_0:def 4;

e in R .edges() by A103, XBOOLE_0:def 4;

then consider n being even Element of NAT such that

A105: 1 <= n and

A106: n <= 7 and

A107: R . n = e by A94, GLIB_001:99;

per cases
( n = 2 or n = 4 or n = 6 )
by A105, A106, Th13;

end;

suppose A108:
n = 2
; :: thesis: contradiction

(2 * 0) + 1 < len R
by A94;

then R . (1 + 1) Joins R . 1,R . (1 + 2),G by GLIB_001:def 3;

then y in Q .vertices() by A98, A104, A107, A108, GLIB_001:105;

then y in A by A80;

hence contradiction by A16, A12, XBOOLE_0:def 4; :: thesis: verum

end;then R . (1 + 1) Joins R . 1,R . (1 + 2),G by GLIB_001:def 3;

then y in Q .vertices() by A98, A104, A107, A108, GLIB_001:105;

then y in A by A80;

hence contradiction by A16, A12, XBOOLE_0:def 4; :: thesis: verum

suppose A109:
n = 4
; :: thesis: contradiction

(2 * 1) + 1 < len R
by A94;

then R . (3 + 1) Joins R . 3,R . (3 + 2),G by GLIB_001:def 3;

then y in Q .vertices() by A98, A104, A107, A109, GLIB_001:105;

then y in A by A80;

hence contradiction by A16, A12, XBOOLE_0:def 4; :: thesis: verum

end;then R . (3 + 1) Joins R . 3,R . (3 + 2),G by GLIB_001:def 3;

then y in Q .vertices() by A98, A104, A107, A109, GLIB_001:105;

then y in A by A80;

hence contradiction by A16, A12, XBOOLE_0:def 4; :: thesis: verum

suppose A110:
n = 6
; :: thesis: contradiction

(2 * 2) + 1 < len R
by A94;

then R . (5 + 1) Joins R . 5,R . (5 + 2),G by GLIB_001:def 3;

then x in Q .vertices() by A99, A104, A107, A110, GLIB_001:105;

then x in A by A80;

hence contradiction by A12, A41, XBOOLE_0:def 4; :: thesis: verum

end;then R . (5 + 1) Joins R . 5,R . (5 + 2),G by GLIB_001:def 3;

then x in Q .vertices() by A99, A104, A107, A110, GLIB_001:105;

then x in A by A80;

hence contradiction by A12, A41, XBOOLE_0:def 4; :: thesis: verum

now :: thesis: for v being object st v in {(Q .first()),(Q .last())} holds

v in (Q .vertices()) /\ (R .vertices())

then A116:
{(Q .first()),(Q .last())} c= (Q .vertices()) /\ (R .vertices())
;v in (Q .vertices()) /\ (R .vertices())

let v be object ; :: thesis: ( v in {(Q .first()),(Q .last())} implies b_{1} in (Q .vertices()) /\ (R .vertices()) )

assume A111: v in {(Q .first()),(Q .last())} ; :: thesis: b_{1} in (Q .vertices()) /\ (R .vertices())

end;assume A111: v in {(Q .first()),(Q .last())} ; :: thesis: b

per cases
( v = Q .first() or v = Q .last() )
by A111, TARSKI:def 2;

end;

suppose A112:
v = Q .first()
; :: thesis: b_{1} in (Q .vertices()) /\ (R .vertices())

then A113:
v in Q .vertices()
by GLIB_001:88;

v in R .vertices() by A94, A100, A112, GLIB_001:87;

hence v in (Q .vertices()) /\ (R .vertices()) by A113, XBOOLE_0:def 4; :: thesis: verum

end;v in R .vertices() by A94, A100, A112, GLIB_001:87;

hence v in (Q .vertices()) /\ (R .vertices()) by A113, XBOOLE_0:def 4; :: thesis: verum

suppose A114:
v = Q .last()
; :: thesis: b_{1} in (Q .vertices()) /\ (R .vertices())

(2 * 0) + 1 <= len R
by A94;

then A115: v in R .vertices() by A97, A114, GLIB_001:87;

v in Q .vertices() by A114, GLIB_001:88;

hence v in (Q .vertices()) /\ (R .vertices()) by A115, XBOOLE_0:def 4; :: thesis: verum

end;then A115: v in R .vertices() by A97, A114, GLIB_001:87;

v in Q .vertices() by A114, GLIB_001:88;

hence v in (Q .vertices()) /\ (R .vertices()) by A115, XBOOLE_0:def 4; :: thesis: verum

now :: thesis: for v being object st v in (Q .vertices()) /\ (R .vertices()) holds

v in {(Q .first()),(Q .last())}

then
(Q .vertices()) /\ (R .vertices()) c= {(Q .first()),(Q .last())}
;v in {(Q .first()),(Q .last())}

let v be object ; :: thesis: ( v in (Q .vertices()) /\ (R .vertices()) implies v in {(Q .first()),(Q .last())} )

assume A117: v in (Q .vertices()) /\ (R .vertices()) ; :: thesis: v in {(Q .first()),(Q .last())}

v in {(Q .last()),y,x,(Q .first())} by A96, A117, XBOOLE_0:def 4;

then A118: ( v = Q .last() or v = y or v = x or v = Q .first() ) by ENUMSET1:def 2;

v in Q .vertices() by A117, XBOOLE_0:def 4;

then v in A by A80;

hence v in {(Q .first()),(Q .last())} by A16, A12, A41, A118, TARSKI:def 2, XBOOLE_0:def 4; :: thesis: verum

end;assume A117: v in (Q .vertices()) /\ (R .vertices()) ; :: thesis: v in {(Q .first()),(Q .last())}

v in {(Q .last()),y,x,(Q .first())} by A96, A117, XBOOLE_0:def 4;

then A118: ( v = Q .last() or v = y or v = x or v = Q .first() ) by ENUMSET1:def 2;

v in Q .vertices() by A117, XBOOLE_0:def 4;

then v in A by A80;

hence v in {(Q .first()),(Q .last())} by A16, A12, A41, A118, TARSKI:def 2, XBOOLE_0:def 4; :: thesis: verum

then A119: (Q .vertices()) /\ (R .vertices()) = {(Q .first()),(Q .last())} by A116;

A120: now :: thesis: for i being odd Nat st i in dom Q & i <> len Q holds

for e being object holds not e Joins Q . i,y,G

A133:
Q .first() = P . k
by A64;for e being object holds not e Joins Q . i,y,G

let i be odd Nat; :: thesis: ( i in dom Q & i <> len Q implies for e being object holds not e Joins Q . i,y,G )

assume that

A121: i in dom Q and

A122: i <> len Q ; :: thesis: for e being object holds not e Joins Q . i,y,G

1 <= i by A121, FINSEQ_3:25;

then 1 + (- 1) <= i + (- 1) by XREAL_1:7;

then reconsider i1 = i - 1 as even Element of NAT by INT_1:3;

reconsider ki1 = k + i1 as odd Element of NAT ;

A123: i + (- 1) < i + (- 0) by XREAL_1:8;

A124: i <= len Q by A121, FINSEQ_3:25;

then A125: i1 < len Q by A123, XXREAL_0:2;

then ki1 in dom P by A50, A51, GLIB_001:36;

then A126: ki1 <= len P by FINSEQ_3:25;

then A127: P . ki1 in A \/ {y} by A31, GLIB_001:7;

then A129: ki1 + 2 <= len P by Th4;

ki1 + 2 <> len P by A53, A122;

then A130: ki1 + 2 < len P by A129, XXREAL_0:1;

A131: P . (len P) in A \/ {y} by A31, GLIB_001:7;

assume A132: ex e being object st e Joins Q . i,y,G ; :: thesis: contradiction

Q . (i1 + 1) = P . ki1 by A50, A51, A125, GLIB_001:36;

hence contradiction by A22, A24, A132, A130, A127, A131, Th19, Th39; :: thesis: verum

end;assume that

A121: i in dom Q and

A122: i <> len Q ; :: thesis: for e being object holds not e Joins Q . i,y,G

1 <= i by A121, FINSEQ_3:25;

then 1 + (- 1) <= i + (- 1) by XREAL_1:7;

then reconsider i1 = i - 1 as even Element of NAT by INT_1:3;

reconsider ki1 = k + i1 as odd Element of NAT ;

A123: i + (- 1) < i + (- 0) by XREAL_1:8;

A124: i <= len Q by A121, FINSEQ_3:25;

then A125: i1 < len Q by A123, XXREAL_0:2;

then ki1 in dom P by A50, A51, GLIB_001:36;

then A126: ki1 <= len P by FINSEQ_3:25;

then A127: P . ki1 in A \/ {y} by A31, GLIB_001:7;

now :: thesis: not ki1 = len P

then
ki1 < len P
by A126, XXREAL_0:1;A128:
((len P) - k) + (- 1) < (len P) - k
by XREAL_1:30;

assume ki1 = len P ; :: thesis: contradiction

hence contradiction by A53, A124, A123, A128, XXREAL_0:2; :: thesis: verum

end;assume ki1 = len P ; :: thesis: contradiction

hence contradiction by A53, A124, A123, A128, XXREAL_0:2; :: thesis: verum

then A129: ki1 + 2 <= len P by Th4;

ki1 + 2 <> len P by A53, A122;

then A130: ki1 + 2 < len P by A129, XXREAL_0:1;

A131: P . (len P) in A \/ {y} by A31, GLIB_001:7;

assume A132: ex e being object st e Joins Q . i,y,G ; :: thesis: contradiction

Q . (i1 + 1) = P . ki1 by A50, A51, A125, GLIB_001:36;

hence contradiction by A22, A24, A132, A130, A127, A131, Th19, Th39; :: thesis: verum

P . k <> P . j by A72, A48, Def3;

then A134: not Q is trivial by A133, A71, GLIB_001:127;

then Q .length() <> 0 ;

then A135: Q .length() >= 0 + 1 by NAT_1:13;

set C = Q .append R;

A136: R .first() = Q .last() by A97;

then A137: (Q .append R) . ((len Q) + 6) = R . (6 + 1) by A94, GLIB_001:33;

A138: (Q .append R) . ((len Q) + 4) = R . (4 + 1) by A94, A136, GLIB_001:33;

A139: (Q .append R) . ((len Q) + 2) = R . (2 + 1) by A94, A136, GLIB_001:33;

(Q .append R) .length() = (Q .length()) + 3 by A95, A136, Th28;

then (Q .append R) .length() >= 1 + 3 by A135, XREAL_1:7;

then A140: (Q .append R) .length() > 3 by NAT_1:13;

A141: R .last() = Q .first() by A94, A100;

then A142: R is open by A73, A136;

then Q .append R is Cycle-like by A74, A136, A141, A101, A102, A119, Th27;

then Q .append R is chordal by A140, Def11;

then consider m, n being odd Nat such that

A143: m + 2 < n and

A144: n <= len (Q .append R) and

(Q .append R) . m <> (Q .append R) . n and

A145: ex e being object st e Joins (Q .append R) . m,(Q .append R) . n,G and

A146: ( Q .append R is Cycle-like implies ( ( not m = 1 or not n = len (Q .append R) ) & ( not m = 1 or not n = (len (Q .append R)) - 2 ) & ( not m = 3 or not n = len (Q .append R) ) ) ) by Th83;

consider e being object such that

A147: e Joins (Q .append R) . m,(Q .append R) . n,G by A145;

A148: ((len (Q .append R)) + 1) + (- 1) = ((len Q) + (len R)) + (- 1) by A136, GLIB_001:28;

A149: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )

proof
end;

A152:
1 <= m
by ABIAN:12;per cases
( n <= len Q or n > len Q )
;

end;

suppose
n <= len Q
; :: thesis: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )

end;

end;

suppose
n > len Q
; :: thesis: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )

then A150:
(len Q) + 2 <= n
by Th4;

end;per cases
( (len Q) + 2 = n or (len Q) + 2 < n )
by A150, XXREAL_0:1;

end;

suppose
(len Q) + 2 = n
; :: thesis: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )

end;

end;

suppose
(len Q) + 2 < n
; :: thesis: ( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )

then A151:
((len Q) + 2) + 2 <= n
by Th4;

end;per cases
( n <= len Q or n = (len Q) + 2 or n = (len Q) + 4 or n = (len Q) + 6 )
by A149;

end;

suppose A153:
n <= len Q
; :: thesis: contradiction

A154:
m + 0 <= m + 2
by XREAL_1:7;

m + 2 <= len Q by A143, A153, XXREAL_0:2;

then m <= len Q by A154, XXREAL_0:2;

then m in dom Q by A152, FINSEQ_3:25;

then A155: Q . m = (Q .append R) . m by GLIB_001:32;

1 <= n by ABIAN:12;

then n in dom Q by A153, FINSEQ_3:25;

then Q . n = (Q .append R) . n by GLIB_001:32;

hence contradiction by A52, A143, A147, A153, A155, Th40; :: thesis: verum

end;m + 2 <= len Q by A143, A153, XXREAL_0:2;

then m <= len Q by A154, XXREAL_0:2;

then m in dom Q by A152, FINSEQ_3:25;

then A155: Q . m = (Q .append R) . m by GLIB_001:32;

1 <= n by ABIAN:12;

then n in dom Q by A153, FINSEQ_3:25;

then Q . n = (Q .append R) . n by GLIB_001:32;

hence contradiction by A52, A143, A147, A153, A155, Th40; :: thesis: verum

suppose A156:
n = (len Q) + 2
; :: thesis: contradiction

then
m < len Q
by A143, XREAL_1:6;

then A157: m in dom Q by A152, FINSEQ_3:25;

then e Joins Q . m,y,G by A98, A139, A147, A156, GLIB_001:32;

hence contradiction by A120, A143, A156, A157; :: thesis: verum

end;then A157: m in dom Q by A152, FINSEQ_3:25;

then e Joins Q . m,y,G by A98, A139, A147, A156, GLIB_001:32;

hence contradiction by A120, A143, A156, A157; :: thesis: verum

suppose A158:
n = (len Q) + 4
; :: thesis: contradiction

then
(m + 2) + 2 <= (len Q) + 4
by A143, Th4;

then m + 4 <= (len Q) + 4 ;

then m <= len Q by XREAL_1:6;

then A159: m in dom Q by A152, FINSEQ_3:25;

then A160: e Joins Q . m,x,G by A99, A138, A147, A158, GLIB_001:32;

end;then m + 4 <= (len Q) + 4 ;

then m <= len Q by XREAL_1:6;

then A159: m in dom Q by A152, FINSEQ_3:25;

then A160: e Joins Q . m,x,G by A99, A138, A147, A158, GLIB_001:32;

suppose A161:
n = (len Q) + 6
; :: thesis: contradiction

then
(m + 2) + 2 <= (len Q) + 6
by A143, Th4;

then m + 4 <= ((len Q) + 2) + 4 ;

then A162: m <= (len Q) + 2 by XREAL_1:6;

end;then m + 4 <= ((len Q) + 2) + 4 ;

then A162: m <= (len Q) + 2 by XREAL_1:6;

per cases
( m < (len Q) + 2 or m = (len Q) + 2 )
by A162, XXREAL_0:1;

end;

suppose A163:
m < (len Q) + 2
; :: thesis: contradiction

A165: m <= len Q by A163, Th4;

then m in dom Q by A152, FINSEQ_3:25;

then (Q .append R) . m = Q . m by GLIB_001:32;

hence contradiction by A52, A100, A137, A147, A161, A165, A164, Th40, GLIB_000:14; :: thesis: verum

end;

now :: thesis: not 1 + 2 >= m

then A164:
((2 * 0) + 1) + 2 < m
;assume
1 + 2 >= m
; :: thesis: contradiction

then m < (2 * 1) + 1 by A74, A94, A136, A141, A101, A142, A102, A119, A148, A146, A161, Th27, XXREAL_0:1;

then m <= 3 - 2 by Th3;

then m < 1 by A74, A94, A136, A141, A101, A142, A102, A119, A148, A146, A161, Th27, XXREAL_0:1;

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

end;then m < (2 * 1) + 1 by A74, A94, A136, A141, A101, A142, A102, A119, A148, A146, A161, Th27, XXREAL_0:1;

then m <= 3 - 2 by Th3;

then m < 1 by A74, A94, A136, A141, A101, A142, A102, A119, A148, A146, A161, Th27, XXREAL_0:1;

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

A165: m <= len Q by A163, Th4;

then m in dom Q by A152, FINSEQ_3:25;

then (Q .append R) . m = Q . m by GLIB_001:32;

hence contradiction by A52, A100, A137, A147, A161, A165, A164, Th40, GLIB_000:14; :: thesis: verum

suppose A166:
m = (len Q) + 2
; :: thesis: contradiction

3 <= len Q
by A134, GLIB_001:125;

then 1 <= len Q by XXREAL_0:2;

then A167: (2 * 0) + 1 in dom Q by FINSEQ_3:25;

1 <> len Q by A72, A48, A64, A70, Def3;

hence contradiction by A120, A98, A100, A137, A139, A147, A161, A166, A167, GLIB_000:14; :: thesis: verum

end;then 1 <= len Q by XXREAL_0:2;

then A167: (2 * 0) + 1 in dom Q by FINSEQ_3:25;

1 <> len Q by A72, A48, A64, A70, Def3;

hence contradiction by A120, A98, A100, A137, A139, A147, A161, A166, A167, GLIB_000:14; :: thesis: verum