let G be 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 & not S is empty holds

for H being inducedSubgraph of G,S holds H is complete

set tVG = the_Vertices_of G;

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 & not S is empty holds

for H being inducedSubgraph of G,S holds H is complete )

assume that

A1: a <> b and

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

for H being inducedSubgraph of G,S holds H is complete

let S be VertexSeparator of a,b; :: thesis: ( S is minimal & not S is empty implies for H being inducedSubgraph of G,S holds H is complete )

assume that

A3: S is minimal and

A4: not S is empty ; :: thesis: for H being inducedSubgraph of G,S holds H is complete

set Gns = the removeVertices of G,S;

reconsider sa = a, sb = b as Vertex of the removeVertices of G,S by A1, A2, Th76;

set A = the removeVertices of G,S .reachableFrom sa;

set B = the removeVertices of G,S .reachableFrom sb;

A5: ( the removeVertices of G,S .reachableFrom sa) /\ ( the removeVertices of G,S .reachableFrom sb) = {} by A1, A2, Th75;

set Gb = the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sb);

set Ga = the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sa);

A6: the_Vertices_of the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sa) = the removeVertices of G,S .reachableFrom sa by GLIB_000:def 37;

A7: the_Vertices_of the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sb) = the removeVertices of G,S .reachableFrom sb by GLIB_000:def 37;

A8: ( the removeVertices of G,S .reachableFrom sb) /\ S = {} by A1, A2, Th74;

A9: ( the removeVertices of G,S .reachableFrom sa) /\ S = {} by A1, A2, Th74;

the_Vertices_of the removeVertices of G,S c= the_Vertices_of G ;

then reconsider A = the removeVertices of G,S .reachableFrom sa, B = the removeVertices of G,S .reachableFrom sb as non empty Subset of (the_Vertices_of G) by XBOOLE_1:1;

let Gs be inducedSubgraph of G,S; :: thesis: Gs is complete

let x, y be Vertex of Gs; :: according to CHORD:def 6 :: thesis: ( x <> y implies x,y are_adjacent )

assume that

A10: x <> y and

A11: not x,y are_adjacent ; :: thesis: contradiction

reconsider xg = x, yg = y as Vertex of G by GLIB_000:42;

A12: S = the_Vertices_of Gs by A4, GLIB_000:def 37;

then A13: ex xag being Vertex of G st

( xag in A & xg,xag are_adjacent ) by A1, A2, A3, Th81;

set Bx = B \/ {xg};

set Ax = A \/ {xg};

set Gbx = the inducedSubgraph of G,(B \/ {xg});

set Gax = the inducedSubgraph of G,(A \/ {xg});

set xy = {xg,yg};

A14: the_Vertices_of the inducedSubgraph of G,(B \/ {xg}) = B \/ {xg} by GLIB_000:def 37;

consider yag being Vertex of G such that

A17: yag in A and

A18: yg,yag are_adjacent by A1, A2, A3, A12, Th81;

A19: yag in A \/ {xg} by A17, XBOOLE_0:def 3;

set Gb1 = the inducedSubgraph of G,((B \/ {x}) \/ {y});

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

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

not a in S by A1, A2, Def8;

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

then reconsider Ga = the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sa) as inducedSubgraph of G,A by A16, Th29;

A22: not y in {x} by A10, TARSKI:def 1;

then reconsider Gb = the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sb) as inducedSubgraph of G,B by A21, Th29;

y in {xg,yg} by TARSKI:def 2;

then A25: y in A \/ {xg,yg} by XBOOLE_0:def 3;

A26: ex xbg being Vertex of G st

( xbg in B & xg,xbg are_adjacent ) by A1, A2, A3, A12, Th82;

not x in B by A24, A12, XBOOLE_0:def 5;

then x in G .AdjacentSet (the_Vertices_of Gb) by A7, A26;

then A27: the inducedSubgraph of G,(B \/ {xg}) is connected by Th56;

y in {xg,yg} by TARSKI:def 2;

then A28: y in B \/ {xg,yg} by XBOOLE_0:def 3;

consider ybg being Vertex of G such that

A29: ybg in B and

A30: yg,ybg are_adjacent by A1, A2, A3, A12, Th82;

A31: (B \/ {x}) \/ {y} = B \/ ({x} \/ {y}) by XBOOLE_1:4

.= B \/ {xg,yg} by ENUMSET1:1 ;

then A32: the_Vertices_of the inducedSubgraph of G,((B \/ {x}) \/ {y}) c= B \/ {xg,yg} by GLIB_000:def 37;

x in {xg,yg} by TARSKI:def 2;

then x in B \/ {xg,yg} by XBOOLE_0:def 3;

then reconsider xb = x, yb = y as Vertex of the inducedSubgraph of G,((B \/ {x}) \/ {y}) by A31, A28, GLIB_000:def 37;

A33: ybg in B \/ {xg} by A29, XBOOLE_0:def 3;

not y in B by A24, A12, XBOOLE_0:def 5;

then not yg in the_Vertices_of the inducedSubgraph of G,(B \/ {xg}) by A14, A22, XBOOLE_0:def 3;

then y in G .AdjacentSet (the_Vertices_of the inducedSubgraph of G,(B \/ {xg})) by A14, A30, A33;

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

then consider Wb being Walk of the inducedSubgraph of G,((B \/ {x}) \/ {y}) such that

A34: Wb is_Walk_from yb,xb ;

not x in A by A16, A12, XBOOLE_0:def 5;

then x in G .AdjacentSet (the_Vertices_of Ga) by A6, A13;

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

A36: (A \/ {x}) \/ {y} = A \/ ({x} \/ {y}) by XBOOLE_1:4

.= A \/ {xg,yg} by ENUMSET1:1 ;

then A37: the_Vertices_of the inducedSubgraph of G,((A \/ {x}) \/ {y}) c= A \/ {xg,yg} by GLIB_000:def 37;

x in {xg,yg} by TARSKI:def 2;

then x in A \/ {xg,yg} by XBOOLE_0:def 3;

then reconsider xa = x, ya = y as Vertex of the inducedSubgraph of G,((A \/ {x}) \/ {y}) by A36, A25, GLIB_000:def 37;

A38: not y in {x} by A10, TARSKI:def 1;

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

then not yg in the_Vertices_of the inducedSubgraph of G,(A \/ {xg}) by A20, A38, XBOOLE_0:def 3;

then y in G .AdjacentSet (the_Vertices_of the inducedSubgraph of G,(A \/ {xg})) by A20, A18, A19;

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

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

A39: Wa is_Walk_from xa,ya ;

A40: (A \/ {xg,yg}) /\ (B \/ {xg,yg}) = (A /\ B) \/ {xg,yg} by XBOOLE_1:24

.= {xg,yg} by A5 ;

A41: Wa .last() = ya by A39;

A42: Wa .first() = xa by A39;

A43: Wb .last() = xa by A34;

A44: Wb .first() = ya by A34;

consider Pb being Path of the inducedSubgraph of G,((B \/ {x}) \/ {y}) such that

A45: Pb is_Walk_from Wb .first() ,Wb .last() and

A46: Pb is minlength by Th38;

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

A47: Pa is_Walk_from Wa .first() ,Wa .last() and

A48: Pa is minlength by Th38;

reconsider Pag = Pa, Pbg = Pb as Path of G by GLIB_001:175;

A49: Pbg . 1 = yg by A44, A45;

Pbg .vertices() = Pb .vertices() by GLIB_001:98;

then A50: Pbg .vertices() c= B \/ {xg,yg} by A32;

Pag .vertices() = Pa .vertices() by GLIB_001:98;

then Pag .vertices() c= A \/ {xg,yg} by A37;

then A51: (Pag .vertices()) /\ (Pbg .vertices()) c= {xg,yg} by A50, A40, XBOOLE_1:27;

set P = Pag .append Pbg;

A52: Pag . (len Pag) = yg by A41, A47;

A53: Pbg . (len Pbg) = xg by A43, A45;

A54: Pbg .last() = Pbg . (len Pbg) ;

then A55: x in Pbg .vertices() by A53, GLIB_001:88;

A56: Pbg .first() = Pbg . 1 ;

then A57: y in Pbg .vertices() by A49, GLIB_001:88;

A58: not Pbg is trivial by A10, A56, A54, A49, A53, GLIB_001:127;

A59: Pbg is open by A10, A49, A53;

A60: not Pbg is Cycle-like by A10, A56, A54, A49, A53, GLIB_001:def 24;

A61: not xg,yg are_adjacent by A4, A11, Th44;

then A62: Pbg .length() >= 2 by A10, A56, A54, A49, A53, Th45;

A63: Pag . 1 = xg by A42, A47;

A64: Pag .edges() misses Pbg .edges()

then A81: x in Pag .vertices() by A63, GLIB_001:88;

A82: Pag .last() = Pag . (len Pag) ;

then A83: (len (Pag .append Pbg)) + 1 = (len Pag) + (len Pbg) by A52, A56, A49, GLIB_001:28;

A84: Pag .length() >= 2 by A10, A61, A80, A82, A63, A52, Th45;

(Pag .append Pbg) .length() = (Pag .length()) + (Pbg .length()) by A82, A52, A56, A49, Th28;

then (Pag .append Pbg) .length() >= 2 + 2 by A84, A62, XREAL_1:7;

then (Pag .append Pbg) .length() >= 3 + 1 ;

then A85: (Pag .append Pbg) .length() > 3 by NAT_1:13;

A86: Pag is open by A10, A63, A52;

A87: y in Pag .vertices() by A82, A52, GLIB_001:88;

{xg,yg} c= (Pag .vertices()) /\ (Pbg .vertices())

then Pag .append Pbg is Cycle-like by A63, A52, A86, A49, A53, A59, A58, A64, Th27;

then Pag .append Pbg is chordal by A85, Def11;

then consider m, n being odd Nat such that

A88: m + 2 < n and

A89: n <= len (Pag .append Pbg) and

A90: (Pag .append Pbg) . m <> (Pag .append Pbg) . n and

A91: ex e being object st e Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G and

A92: for f being object st f in (Pag .append Pbg) .edges() holds

not f Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G ;

A93: m < n by A88, NAT_1:12;

consider e being object such that

A94: e Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G by A91;

A95: e Joins (Pag .append Pbg) . n,(Pag .append Pbg) . m,G by A94;

A96: m in NAT by ORDINAL1:def 12;

A97: not Pag is Cycle-like by A10, A80, A82, A63, A52, GLIB_001:def 24;

A98: 1 <= n by ABIAN:12;

A99: 1 <= m by ABIAN:12;

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

for H being inducedSubgraph of G,S holds H is complete

set tVG = the_Vertices_of G;

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 & not S is empty holds

for H being inducedSubgraph of G,S holds H is complete )

assume that

A1: a <> b and

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

for H being inducedSubgraph of G,S holds H is complete

let S be VertexSeparator of a,b; :: thesis: ( S is minimal & not S is empty implies for H being inducedSubgraph of G,S holds H is complete )

assume that

A3: S is minimal and

A4: not S is empty ; :: thesis: for H being inducedSubgraph of G,S holds H is complete

set Gns = the removeVertices of G,S;

reconsider sa = a, sb = b as Vertex of the removeVertices of G,S by A1, A2, Th76;

set A = the removeVertices of G,S .reachableFrom sa;

set B = the removeVertices of G,S .reachableFrom sb;

A5: ( the removeVertices of G,S .reachableFrom sa) /\ ( the removeVertices of G,S .reachableFrom sb) = {} by A1, A2, Th75;

set Gb = the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sb);

set Ga = the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sa);

A6: the_Vertices_of the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sa) = the removeVertices of G,S .reachableFrom sa by GLIB_000:def 37;

A7: the_Vertices_of the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sb) = the removeVertices of G,S .reachableFrom sb by GLIB_000:def 37;

A8: ( the removeVertices of G,S .reachableFrom sb) /\ S = {} by A1, A2, Th74;

A9: ( the removeVertices of G,S .reachableFrom sa) /\ S = {} by A1, A2, Th74;

the_Vertices_of the removeVertices of G,S c= the_Vertices_of G ;

then reconsider A = the removeVertices of G,S .reachableFrom sa, B = the removeVertices of G,S .reachableFrom sb as non empty Subset of (the_Vertices_of G) by XBOOLE_1:1;

let Gs be inducedSubgraph of G,S; :: thesis: Gs is complete

let x, y be Vertex of Gs; :: according to CHORD:def 6 :: thesis: ( x <> y implies x,y are_adjacent )

assume that

A10: x <> y and

A11: not x,y are_adjacent ; :: thesis: contradiction

reconsider xg = x, yg = y as Vertex of G by GLIB_000:42;

A12: S = the_Vertices_of Gs by A4, GLIB_000:def 37;

then A13: ex xag being Vertex of G st

( xag in A & xg,xag are_adjacent ) by A1, A2, A3, Th81;

set Bx = B \/ {xg};

set Ax = A \/ {xg};

set Gbx = the inducedSubgraph of G,(B \/ {xg});

set Gax = the inducedSubgraph of G,(A \/ {xg});

set xy = {xg,yg};

A14: the_Vertices_of the inducedSubgraph of G,(B \/ {xg}) = B \/ {xg} by GLIB_000:def 37;

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

x in (the_Vertices_of G) \ S

then A16:
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 A9, 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 A9, A15, XBOOLE_0:def 4;

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

consider yag being Vertex of G such that

A17: yag in A and

A18: yg,yag are_adjacent by A1, A2, A3, A12, Th81;

A19: yag in A \/ {xg} by A17, XBOOLE_0:def 3;

set Gb1 = the inducedSubgraph of G,((B \/ {x}) \/ {y});

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

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

not a in S by A1, A2, Def8;

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

then reconsider Ga = the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sa) as inducedSubgraph of G,A by A16, Th29;

A22: not y in {x} by A10, TARSKI:def 1;

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

x in (the_Vertices_of G) \ S

then A24:
B c= (the_Vertices_of G) \ S
;x in (the_Vertices_of G) \ S

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

assume A23: x in B ; :: thesis: x in (the_Vertices_of G) \ S

not x in S by A8, A23, XBOOLE_0:def 4;

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

end;assume A23: x in B ; :: thesis: x in (the_Vertices_of G) \ S

not x in S by A8, A23, XBOOLE_0:def 4;

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

then reconsider Gb = the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sb) as inducedSubgraph of G,B by A21, Th29;

y in {xg,yg} by TARSKI:def 2;

then A25: y in A \/ {xg,yg} by XBOOLE_0:def 3;

A26: ex xbg being Vertex of G st

( xbg in B & xg,xbg are_adjacent ) by A1, A2, A3, A12, Th82;

not x in B by A24, A12, XBOOLE_0:def 5;

then x in G .AdjacentSet (the_Vertices_of Gb) by A7, A26;

then A27: the inducedSubgraph of G,(B \/ {xg}) is connected by Th56;

y in {xg,yg} by TARSKI:def 2;

then A28: y in B \/ {xg,yg} by XBOOLE_0:def 3;

consider ybg being Vertex of G such that

A29: ybg in B and

A30: yg,ybg are_adjacent by A1, A2, A3, A12, Th82;

A31: (B \/ {x}) \/ {y} = B \/ ({x} \/ {y}) by XBOOLE_1:4

.= B \/ {xg,yg} by ENUMSET1:1 ;

then A32: the_Vertices_of the inducedSubgraph of G,((B \/ {x}) \/ {y}) c= B \/ {xg,yg} by GLIB_000:def 37;

x in {xg,yg} by TARSKI:def 2;

then x in B \/ {xg,yg} by XBOOLE_0:def 3;

then reconsider xb = x, yb = y as Vertex of the inducedSubgraph of G,((B \/ {x}) \/ {y}) by A31, A28, GLIB_000:def 37;

A33: ybg in B \/ {xg} by A29, XBOOLE_0:def 3;

not y in B by A24, A12, XBOOLE_0:def 5;

then not yg in the_Vertices_of the inducedSubgraph of G,(B \/ {xg}) by A14, A22, XBOOLE_0:def 3;

then y in G .AdjacentSet (the_Vertices_of the inducedSubgraph of G,(B \/ {xg})) by A14, A30, A33;

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

then consider Wb being Walk of the inducedSubgraph of G,((B \/ {x}) \/ {y}) such that

A34: Wb is_Walk_from yb,xb ;

not x in A by A16, A12, XBOOLE_0:def 5;

then x in G .AdjacentSet (the_Vertices_of Ga) by A6, A13;

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

A36: (A \/ {x}) \/ {y} = A \/ ({x} \/ {y}) by XBOOLE_1:4

.= A \/ {xg,yg} by ENUMSET1:1 ;

then A37: the_Vertices_of the inducedSubgraph of G,((A \/ {x}) \/ {y}) c= A \/ {xg,yg} by GLIB_000:def 37;

x in {xg,yg} by TARSKI:def 2;

then x in A \/ {xg,yg} by XBOOLE_0:def 3;

then reconsider xa = x, ya = y as Vertex of the inducedSubgraph of G,((A \/ {x}) \/ {y}) by A36, A25, GLIB_000:def 37;

A38: not y in {x} by A10, TARSKI:def 1;

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

then not yg in the_Vertices_of the inducedSubgraph of G,(A \/ {xg}) by A20, A38, XBOOLE_0:def 3;

then y in G .AdjacentSet (the_Vertices_of the inducedSubgraph of G,(A \/ {xg})) by A20, A18, A19;

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

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

A39: Wa is_Walk_from xa,ya ;

A40: (A \/ {xg,yg}) /\ (B \/ {xg,yg}) = (A /\ B) \/ {xg,yg} by XBOOLE_1:24

.= {xg,yg} by A5 ;

A41: Wa .last() = ya by A39;

A42: Wa .first() = xa by A39;

A43: Wb .last() = xa by A34;

A44: Wb .first() = ya by A34;

consider Pb being Path of the inducedSubgraph of G,((B \/ {x}) \/ {y}) such that

A45: Pb is_Walk_from Wb .first() ,Wb .last() and

A46: Pb is minlength by Th38;

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

A47: Pa is_Walk_from Wa .first() ,Wa .last() and

A48: Pa is minlength by Th38;

reconsider Pag = Pa, Pbg = Pb as Path of G by GLIB_001:175;

A49: Pbg . 1 = yg by A44, A45;

Pbg .vertices() = Pb .vertices() by GLIB_001:98;

then A50: Pbg .vertices() c= B \/ {xg,yg} by A32;

Pag .vertices() = Pa .vertices() by GLIB_001:98;

then Pag .vertices() c= A \/ {xg,yg} by A37;

then A51: (Pag .vertices()) /\ (Pbg .vertices()) c= {xg,yg} by A50, A40, XBOOLE_1:27;

set P = Pag .append Pbg;

A52: Pag . (len Pag) = yg by A41, A47;

A53: Pbg . (len Pbg) = xg by A43, A45;

A54: Pbg .last() = Pbg . (len Pbg) ;

then A55: x in Pbg .vertices() by A53, GLIB_001:88;

A56: Pbg .first() = Pbg . 1 ;

then A57: y in Pbg .vertices() by A49, GLIB_001:88;

A58: not Pbg is trivial by A10, A56, A54, A49, A53, GLIB_001:127;

A59: Pbg is open by A10, A49, A53;

A60: not Pbg is Cycle-like by A10, A56, A54, A49, A53, GLIB_001:def 24;

A61: not xg,yg are_adjacent by A4, A11, Th44;

then A62: Pbg .length() >= 2 by A10, A56, A54, A49, A53, Th45;

A63: Pag . 1 = xg by A42, A47;

A64: Pag .edges() misses Pbg .edges()

proof

A80:
Pag .first() = Pag . 1
;
assume
(Pag .edges()) /\ (Pbg .edges()) <> {}
; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider e being object such that

A65: e in (Pag .edges()) /\ (Pbg .edges()) by XBOOLE_0:def 1;

e in Pag .edges() by A65, XBOOLE_0:def 4;

then e in Pa .edges() by GLIB_001:110;

then consider a1, a2 being Vertex of the inducedSubgraph of G,((A \/ {x}) \/ {y}), na being odd Element of NAT such that

A66: na + 2 <= len Pag and

A67: a1 = Pag . na and

e = Pag . (na + 1) and

A68: a2 = Pag . (na + 2) and

A69: e Joins a1,a2, the inducedSubgraph of G,((A \/ {x}) \/ {y}) by GLIB_001:103;

A70: e Joins a1,a2,G by A69, GLIB_000:72;

e in Pbg .edges() by A65, XBOOLE_0:def 4;

then e in Pb .edges() by GLIB_001:110;

then consider b1, b2 being Vertex of the inducedSubgraph of G,((B \/ {x}) \/ {y}), nb being odd Element of NAT such that

nb + 2 <= len Pbg and

b1 = Pbg . nb and

e = Pbg . (nb + 1) and

b2 = Pbg . (nb + 2) and

A71: e Joins b1,b2, the inducedSubgraph of G,((B \/ {x}) \/ {y}) by GLIB_001:103;

A72: the_Vertices_of the inducedSubgraph of G,((B \/ {x}) \/ {y}) = B \/ {xg,yg} by A31, GLIB_000:def 37;

e Joins b1,b2,G by A71, GLIB_000:72;

then A73: ( ( a1 = b1 & a2 = b2 ) or ( a1 = b2 & a2 = b1 ) ) by A70;

then A74: ( a1 in B or a1 in {xg,yg} ) by A72, XBOOLE_0:def 3;

A75: the_Vertices_of the inducedSubgraph of G,((A \/ {x}) \/ {y}) = A \/ {xg,yg} by A36, GLIB_000:def 37;

then A76: ( a1 in A or a1 in {xg,yg} ) by XBOOLE_0:def 3;

A77: ( a2 in A or a2 in {xg,yg} ) by A75, XBOOLE_0:def 3;

A78: ( a2 in B or a2 in {xg,yg} ) by A73, A72, XBOOLE_0:def 3;

end;then consider e being object such that

A65: e in (Pag .edges()) /\ (Pbg .edges()) by XBOOLE_0:def 1;

e in Pag .edges() by A65, XBOOLE_0:def 4;

then e in Pa .edges() by GLIB_001:110;

then consider a1, a2 being Vertex of the inducedSubgraph of G,((A \/ {x}) \/ {y}), na being odd Element of NAT such that

A66: na + 2 <= len Pag and

A67: a1 = Pag . na and

e = Pag . (na + 1) and

A68: a2 = Pag . (na + 2) and

A69: e Joins a1,a2, the inducedSubgraph of G,((A \/ {x}) \/ {y}) by GLIB_001:103;

A70: e Joins a1,a2,G by A69, GLIB_000:72;

e in Pbg .edges() by A65, XBOOLE_0:def 4;

then e in Pb .edges() by GLIB_001:110;

then consider b1, b2 being Vertex of the inducedSubgraph of G,((B \/ {x}) \/ {y}), nb being odd Element of NAT such that

nb + 2 <= len Pbg and

b1 = Pbg . nb and

e = Pbg . (nb + 1) and

b2 = Pbg . (nb + 2) and

A71: e Joins b1,b2, the inducedSubgraph of G,((B \/ {x}) \/ {y}) by GLIB_001:103;

A72: the_Vertices_of the inducedSubgraph of G,((B \/ {x}) \/ {y}) = B \/ {xg,yg} by A31, GLIB_000:def 37;

e Joins b1,b2,G by A71, GLIB_000:72;

then A73: ( ( a1 = b1 & a2 = b2 ) or ( a1 = b2 & a2 = b1 ) ) by A70;

then A74: ( a1 in B or a1 in {xg,yg} ) by A72, XBOOLE_0:def 3;

A75: the_Vertices_of the inducedSubgraph of G,((A \/ {x}) \/ {y}) = A \/ {xg,yg} by A36, GLIB_000:def 37;

then A76: ( a1 in A or a1 in {xg,yg} ) by XBOOLE_0:def 3;

A77: ( a2 in A or a2 in {xg,yg} ) by A75, XBOOLE_0:def 3;

A78: ( a2 in B or a2 in {xg,yg} ) by A73, A72, XBOOLE_0:def 3;

per cases
( ( a1 = x & a2 = x ) or ( a1 = y & a2 = y ) or ( a1 = x & a2 = y ) or ( a1 = y & a2 = x ) )
by A5, A76, A77, A74, A78, TARSKI:def 2, XBOOLE_0:def 4;

end;

suppose A79:
( ( a1 = x & a2 = x ) or ( a1 = y & a2 = y ) )
; :: thesis: contradiction

na < na + 2
by XREAL_1:39;

hence contradiction by A10, A63, A52, A66, A67, A68, A79, GLIB_001:def 28; :: thesis: verum

end;hence contradiction by A10, A63, A52, A66, A67, A68, A79, GLIB_001:def 28; :: thesis: verum

then A81: x in Pag .vertices() by A63, GLIB_001:88;

A82: Pag .last() = Pag . (len Pag) ;

then A83: (len (Pag .append Pbg)) + 1 = (len Pag) + (len Pbg) by A52, A56, A49, GLIB_001:28;

A84: Pag .length() >= 2 by A10, A61, A80, A82, A63, A52, Th45;

(Pag .append Pbg) .length() = (Pag .length()) + (Pbg .length()) by A82, A52, A56, A49, Th28;

then (Pag .append Pbg) .length() >= 2 + 2 by A84, A62, XREAL_1:7;

then (Pag .append Pbg) .length() >= 3 + 1 ;

then A85: (Pag .append Pbg) .length() > 3 by NAT_1:13;

A86: Pag is open by A10, A63, A52;

A87: y in Pag .vertices() by A82, A52, GLIB_001:88;

{xg,yg} c= (Pag .vertices()) /\ (Pbg .vertices())

proof

then
(Pag .vertices()) /\ (Pbg .vertices()) = {xg,yg}
by A51;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {xg,yg} or a in (Pag .vertices()) /\ (Pbg .vertices()) )

assume a in {xg,yg} ; :: thesis: a in (Pag .vertices()) /\ (Pbg .vertices())

then ( a = x or a = y ) by TARSKI:def 2;

hence a in (Pag .vertices()) /\ (Pbg .vertices()) by A81, A87, A55, A57, XBOOLE_0:def 4; :: thesis: verum

end;assume a in {xg,yg} ; :: thesis: a in (Pag .vertices()) /\ (Pbg .vertices())

then ( a = x or a = y ) by TARSKI:def 2;

hence a in (Pag .vertices()) /\ (Pbg .vertices()) by A81, A87, A55, A57, XBOOLE_0:def 4; :: thesis: verum

then Pag .append Pbg is Cycle-like by A63, A52, A86, A49, A53, A59, A58, A64, Th27;

then Pag .append Pbg is chordal by A85, Def11;

then consider m, n being odd Nat such that

A88: m + 2 < n and

A89: n <= len (Pag .append Pbg) and

A90: (Pag .append Pbg) . m <> (Pag .append Pbg) . n and

A91: ex e being object st e Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G and

A92: for f being object st f in (Pag .append Pbg) .edges() holds

not f Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G ;

A93: m < n by A88, NAT_1:12;

consider e being object such that

A94: e Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G by A91;

A95: e Joins (Pag .append Pbg) . n,(Pag .append Pbg) . m,G by A94;

A96: m in NAT by ORDINAL1:def 12;

A97: not Pag is Cycle-like by A10, A80, A82, A63, A52, GLIB_001:def 24;

A98: 1 <= n by ABIAN:12;

A99: 1 <= m by ABIAN:12;

per cases
( ( m < len Pag & n <= len Pag ) or ( m < len Pag & len Pag < n ) or len Pag <= m )
;

end;

suppose A100:
( m < len Pag & n <= len Pag )
; :: thesis: contradiction

then
n in dom Pag
by A98, FINSEQ_3:25;

then A101: (Pag .append Pbg) . n = Pag . n by GLIB_001:32;

m in dom Pag by A99, A100, FINSEQ_3:25;

then (Pag .append Pbg) . m = Pag . m by GLIB_001:32;

then Pag is chordal by A97, A88, A91, A100, A101, Th84;

then Pa is chordal by A36, Th86;

hence contradiction by A48, Th88; :: thesis: verum

end;then A101: (Pag .append Pbg) . n = Pag . n by GLIB_001:32;

m in dom Pag by A99, A100, FINSEQ_3:25;

then (Pag .append Pbg) . m = Pag . m by GLIB_001:32;

then Pag is chordal by A97, A88, A91, A100, A101, Th84;

then Pa is chordal by A36, Th86;

hence contradiction by A48, Th88; :: thesis: verum

suppose A102:
( m < len Pag & len Pag < n )
; :: thesis: contradiction

then A103:
Pag . m in the_Vertices_of the inducedSubgraph of G,((A \/ {x}) \/ {y})
by A96, GLIB_001:7;

m in dom Pag by A99, A102, FINSEQ_3:25;

then A104: (Pag .append Pbg) . m = Pag . m by GLIB_001:32;

A105: not n in dom Pag by A102, FINSEQ_3:25;

n in dom (Pag .append Pbg) by A89, A98, FINSEQ_3:25;

then consider n1 being Element of NAT such that

A106: n1 < len Pbg and

A107: n = (len Pag) + n1 by A105, GLIB_001:34;

A108: (Pag .append Pbg) . ((len Pag) + n1) = Pbg . (n1 + 1) by A82, A52, A56, A49, A106, GLIB_001:33;

reconsider n1 = n1 as even Element of NAT by A107;

reconsider n11 = n1 + 1 as odd Element of NAT ;

A109: n11 <= len Pbg by A106, NAT_1:13;

then A110: Pbg . n11 in the_Vertices_of the inducedSubgraph of G,((B \/ {x}) \/ {y}) by GLIB_001:7;

end;m in dom Pag by A99, A102, FINSEQ_3:25;

then A104: (Pag .append Pbg) . m = Pag . m by GLIB_001:32;

A105: not n in dom Pag by A102, FINSEQ_3:25;

n in dom (Pag .append Pbg) by A89, A98, FINSEQ_3:25;

then consider n1 being Element of NAT such that

A106: n1 < len Pbg and

A107: n = (len Pag) + n1 by A105, GLIB_001:34;

A108: (Pag .append Pbg) . ((len Pag) + n1) = Pbg . (n1 + 1) by A82, A52, A56, A49, A106, GLIB_001:33;

reconsider n1 = n1 as even Element of NAT by A107;

reconsider n11 = n1 + 1 as odd Element of NAT ;

A109: n11 <= len Pbg by A106, NAT_1:13;

then A110: Pbg . n11 in the_Vertices_of the inducedSubgraph of G,((B \/ {x}) \/ {y}) by GLIB_001:7;

per cases
( ( Pag . m in A & Pbg . n11 in {xg,yg} ) or ( Pag . m in A & Pbg . n11 in B ) or ( Pag . m in {xg,yg} & Pbg . n11 in B ) or ( Pag . m in {xg,yg} & Pbg . n11 in {xg,yg} ) )
by A37, A32, A103, A110, XBOOLE_0:def 3;

end;

suppose A111:
( Pag . m in A & Pbg . n11 in {xg,yg} )
; :: thesis: contradiction

end;

per cases
( Pbg . n11 = Pag . 1 or Pbg . n11 = Pag . (len Pag) )
by A63, A52, A111, TARSKI:def 2;

end;

suppose A112:
Pbg . n11 = Pag . 1
; :: thesis: contradiction

then Pa is chordal by A36, Th86;

hence contradiction by A48, Th88; :: thesis: verum

end;

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

then
Pag is chordal
by A97, A95, A102, A104, A107, A108, A112, Th84, JORDAN12:2;assume A113:
1 + 2 >= m
; :: thesis: contradiction

end;per cases
( 1 + 2 > m or 1 + 2 = m )
by A113, XXREAL_0:1;

end;

suppose
1 + 2 > m
; :: thesis: contradiction

then
1 >= m
by Th4, JORDAN12:2;

hence contradiction by A90, A99, A104, A107, A108, A112, XXREAL_0:1; :: thesis: verum

end;hence contradiction by A90, A99, A104, A107, A108, A112, XXREAL_0:1; :: thesis: verum

suppose A114:
1 + 2 = m
; :: thesis: contradiction

then A115:
1 + 1 < len Pag
by A102, XXREAL_0:2;

then 1 + 1 in dom Pag by FINSEQ_3:25;

then A116: Pag . (1 + 1) = (Pag .append Pbg) . (1 + 1) by GLIB_001:32;

1 < (len Pag) - 1 by A115, XREAL_1:20;

then 1 + 0 < ((len Pag) - 1) + (len Pbg) by XREAL_1:8;

then A117: (Pag .append Pbg) . (1 + 1) in (Pag .append Pbg) .edges() by A83, GLIB_001:100, JORDAN12:2;

1 < len Pag by A99, A102, XXREAL_0:2;

then Pag . (1 + 1) Joins Pag . 1,Pag . m,G by A114, GLIB_001:def 3, JORDAN12:2;

hence contradiction by A92, A104, A107, A108, A112, A116, A117, GLIB_000:14; :: thesis: verum

end;then 1 + 1 in dom Pag by FINSEQ_3:25;

then A116: Pag . (1 + 1) = (Pag .append Pbg) . (1 + 1) by GLIB_001:32;

1 < (len Pag) - 1 by A115, XREAL_1:20;

then 1 + 0 < ((len Pag) - 1) + (len Pbg) by XREAL_1:8;

then A117: (Pag .append Pbg) . (1 + 1) in (Pag .append Pbg) .edges() by A83, GLIB_001:100, JORDAN12:2;

1 < len Pag by A99, A102, XXREAL_0:2;

then Pag . (1 + 1) Joins Pag . 1,Pag . m,G by A114, GLIB_001:def 3, JORDAN12:2;

hence contradiction by A92, A104, A107, A108, A112, A116, A117, GLIB_000:14; :: thesis: verum

then Pa is chordal by A36, Th86;

hence contradiction by A48, Th88; :: thesis: verum

suppose A118:
Pbg . n11 = Pag . (len Pag)
; :: thesis: contradiction

then Pa is chordal by A36, Th86;

hence contradiction by A48, Th88; :: thesis: verum

end;

now :: thesis: not m + 2 >= len Pag

then
Pag is chordal
by A97, A91, A104, A107, A108, A118, Th84;set L = len Pag;

assume A119: m + 2 >= len Pag ; :: thesis: contradiction

end;assume A119: m + 2 >= len Pag ; :: thesis: contradiction

per cases
( m + 2 = len Pag or m + 2 > len Pag )
by A119, XXREAL_0:1;

end;

suppose A120:
m + 2 = len Pag
; :: thesis: contradiction

then A121:
len Pag = (m + 1) + 1
;

then A122: m + 1 < len Pag by NAT_1:13;

1 <= m + 1 by NAT_1:12;

then m + 1 in dom Pag by A122, FINSEQ_3:25;

then A123: Pag . (m + 1) = (Pag .append Pbg) . (m + 1) by GLIB_001:32;

m < (len Pag) - 1 by A121, NAT_1:13;

then m + 0 < ((len Pag) - 1) + (len Pbg) by XREAL_1:8;

then A124: (Pag .append Pbg) . (m + 1) in (Pag .append Pbg) .edges() by A83, GLIB_001:100;

m < len Pag by A122, NAT_1:13;

then Pag . (m + 1) Joins Pag . m,Pag . (len Pag),G by A96, A120, GLIB_001:def 3;

hence contradiction by A92, A104, A107, A108, A118, A123, A124; :: thesis: verum

end;then A122: m + 1 < len Pag by NAT_1:13;

1 <= m + 1 by NAT_1:12;

then m + 1 in dom Pag by A122, FINSEQ_3:25;

then A123: Pag . (m + 1) = (Pag .append Pbg) . (m + 1) by GLIB_001:32;

m < (len Pag) - 1 by A121, NAT_1:13;

then m + 0 < ((len Pag) - 1) + (len Pbg) by XREAL_1:8;

then A124: (Pag .append Pbg) . (m + 1) in (Pag .append Pbg) .edges() by A83, GLIB_001:100;

m < len Pag by A122, NAT_1:13;

then Pag . (m + 1) Joins Pag . m,Pag . (len Pag),G by A96, A120, GLIB_001:def 3;

hence contradiction by A92, A104, A107, A108, A118, A123, A124; :: thesis: verum

then Pa is chordal by A36, Th86;

hence contradiction by A48, Th88; :: thesis: verum

suppose A125:
( Pag . m in A & Pbg . n11 in B )
; :: thesis: contradiction

then reconsider bc = Pb . n11 as Vertex of Gb by GLIB_000:def 37;

reconsider ac = Pa . m as Vertex of Ga by A125, GLIB_000:def 37;

set WAB = the removeVertices of G,S .walkOf (ac,e,bc);

e Joins ac,bc, the removeVertices of G,S by A16, A24, A94, A104, A107, A108, A125, Th19;

then A126: the removeVertices of G,S .walkOf (ac,e,bc) is_Walk_from ac,bc by GLIB_001:15;

b in B by GLIB_002:9;

then reconsider bb = b as Vertex of Gb by GLIB_000:def 37;

a in A by GLIB_002:9;

then reconsider aa = a as Vertex of Ga by GLIB_000:def 37;

consider WA being Walk of Ga such that

A127: WA is_Walk_from aa,ac by GLIB_002:def 1;

consider WB being Walk of Gb such that

A128: WB is_Walk_from bc,bb by GLIB_002:def 1;

reconsider WA = WA, WB = WB as Walk of the removeVertices of G,S by GLIB_001:167;

reconsider WAs = WA, WBs = WB as Walk of the removeVertices of G,S ;

A129: WBs is_Walk_from bc,bb by A128;

set WaB = WAs .append ( the removeVertices of G,S .walkOf (ac,e,bc));

set Wab = (WAs .append ( the removeVertices of G,S .walkOf (ac,e,bc))) .append WBs;

WAs is_Walk_from aa,ac by A127;

then WAs .append ( the removeVertices of G,S .walkOf (ac,e,bc)) is_Walk_from aa,bc by A126, GLIB_001:31;

then (WAs .append ( the removeVertices of G,S .walkOf (ac,e,bc))) .append WBs is_Walk_from a,b by A129, GLIB_001:31;

hence contradiction by A1, A2, Def8; :: thesis: verum

end;reconsider ac = Pa . m as Vertex of Ga by A125, GLIB_000:def 37;

set WAB = the removeVertices of G,S .walkOf (ac,e,bc);

e Joins ac,bc, the removeVertices of G,S by A16, A24, A94, A104, A107, A108, A125, Th19;

then A126: the removeVertices of G,S .walkOf (ac,e,bc) is_Walk_from ac,bc by GLIB_001:15;

b in B by GLIB_002:9;

then reconsider bb = b as Vertex of Gb by GLIB_000:def 37;

a in A by GLIB_002:9;

then reconsider aa = a as Vertex of Ga by GLIB_000:def 37;

consider WA being Walk of Ga such that

A127: WA is_Walk_from aa,ac by GLIB_002:def 1;

consider WB being Walk of Gb such that

A128: WB is_Walk_from bc,bb by GLIB_002:def 1;

reconsider WA = WA, WB = WB as Walk of the removeVertices of G,S by GLIB_001:167;

reconsider WAs = WA, WBs = WB as Walk of the removeVertices of G,S ;

A129: WBs is_Walk_from bc,bb by A128;

set WaB = WAs .append ( the removeVertices of G,S .walkOf (ac,e,bc));

set Wab = (WAs .append ( the removeVertices of G,S .walkOf (ac,e,bc))) .append WBs;

WAs is_Walk_from aa,ac by A127;

then WAs .append ( the removeVertices of G,S .walkOf (ac,e,bc)) is_Walk_from aa,bc by A126, GLIB_001:31;

then (WAs .append ( the removeVertices of G,S .walkOf (ac,e,bc))) .append WBs is_Walk_from a,b by A129, GLIB_001:31;

hence contradiction by A1, A2, Def8; :: thesis: verum

suppose
( Pag . m in {xg,yg} & Pbg . n11 in B )
; :: thesis: contradiction

then
( Pag . m = x or Pag . m = y )
by TARSKI:def 2;

then A130: Pag . m = x by A63, A52, A96, A102, GLIB_001:def 28

.= Pbg . (len Pbg) by A43, A45 ;

then Pb is chordal by A31, Th86;

hence contradiction by A46, Th88; :: thesis: verum

end;then A130: Pag . m = x by A63, A52, A96, A102, GLIB_001:def 28

.= Pbg . (len Pbg) by A43, A45 ;

now :: thesis: not n11 + 2 >= len Pbg

then
Pbg is chordal
by A60, A95, A104, A107, A108, A130, Th84;set L = len Pbg;

assume A131: n11 + 2 >= len Pbg ; :: thesis: contradiction

end;assume A131: n11 + 2 >= len Pbg ; :: thesis: contradiction

per cases
( n11 + 2 = len Pbg or n11 + 2 > len Pbg )
by A131, XXREAL_0:1;

end;

suppose A132:
n11 + 2 = len Pbg
; :: thesis: contradiction

then A133:
len Pbg = (n11 + 1) + 1
;

then n11 < (len Pbg) - 1 by NAT_1:13;

then A134: (len Pag) + n11 < ((len Pbg) - 1) + (len Pag) by XREAL_1:6;

n11 + 1 < len Pbg by A133, NAT_1:13;

then A135: n11 < len Pbg by NAT_1:13;

then Pbg . (n11 + 1) Joins Pbg . n11,Pbg . (len Pbg), the inducedSubgraph of G,((B \/ {x}) \/ {y}) by A132, GLIB_001:def 3;

then Pbg . (n11 + 1) Joins Pbg . (len Pbg),Pbg . n11, the inducedSubgraph of G,((B \/ {x}) \/ {y}) ;

then A136: Pbg . (n11 + 1) Joins Pbg . (len Pbg),Pbg . n11,G by GLIB_000:72;

A137: 1 <= (len Pag) + n11 by ABIAN:12, NAT_1:12;

Pbg . (n11 + 1) = (Pag .append Pbg) . ((len Pag) + n11) by A82, A52, A56, A49, A135, GLIB_001:33;

then Pbg . (n11 + 1) in (Pag .append Pbg) .edges() by A83, A137, A134, GLIB_001:99;

hence contradiction by A92, A104, A107, A108, A130, A136; :: thesis: verum

end;then n11 < (len Pbg) - 1 by NAT_1:13;

then A134: (len Pag) + n11 < ((len Pbg) - 1) + (len Pag) by XREAL_1:6;

n11 + 1 < len Pbg by A133, NAT_1:13;

then A135: n11 < len Pbg by NAT_1:13;

then Pbg . (n11 + 1) Joins Pbg . n11,Pbg . (len Pbg), the inducedSubgraph of G,((B \/ {x}) \/ {y}) by A132, GLIB_001:def 3;

then Pbg . (n11 + 1) Joins Pbg . (len Pbg),Pbg . n11, the inducedSubgraph of G,((B \/ {x}) \/ {y}) ;

then A136: Pbg . (n11 + 1) Joins Pbg . (len Pbg),Pbg . n11,G by GLIB_000:72;

A137: 1 <= (len Pag) + n11 by ABIAN:12, NAT_1:12;

Pbg . (n11 + 1) = (Pag .append Pbg) . ((len Pag) + n11) by A82, A52, A56, A49, A135, GLIB_001:33;

then Pbg . (n11 + 1) in (Pag .append Pbg) .edges() by A83, A137, A134, GLIB_001:99;

hence contradiction by A92, A104, A107, A108, A130, A136; :: thesis: verum

suppose
n11 + 2 > len Pbg
; :: thesis: contradiction

then
n11 >= len Pbg
by Th4;

hence contradiction by A90, A104, A107, A108, A109, A130, XXREAL_0:1; :: thesis: verum

end;hence contradiction by A90, A104, A107, A108, A109, A130, XXREAL_0:1; :: thesis: verum

then Pb is chordal by A31, Th86;

hence contradiction by A46, Th88; :: thesis: verum

suppose A138:
( Pag . m in {xg,yg} & Pbg . n11 in {xg,yg} )
; :: thesis: contradiction

then A139:
( Pbg . n11 = x or Pbg . n11 = y )
by TARSKI:def 2;

( Pag . m = x or Pag . m = y ) by A138, TARSKI:def 2;

then xg,yg are_adjacent by A90, A91, A104, A107, A108, A139, Def3;

hence contradiction by A4, A11, Th44; :: thesis: verum

end;( Pag . m = x or Pag . m = y ) by A138, TARSKI:def 2;

then xg,yg are_adjacent by A90, A91, A104, A107, A108, A139, Def3;

hence contradiction by A4, A11, Th44; :: thesis: verum

suppose A140:
len Pag <= m
; :: thesis: contradiction

then consider m1 being Nat such that

A141: m = (len Pag) + m1 by NAT_1:10;

n > len Pag by A93, A140, XXREAL_0:2;

then A142: not n in dom Pag by FINSEQ_3:25;

n in dom (Pag .append Pbg) by A89, A98, FINSEQ_3:25;

then consider n1 being Element of NAT such that

A143: n1 < len Pbg and

A144: n = (len Pag) + n1 by A142, GLIB_001:34;

A145: (Pag .append Pbg) . ((len Pag) + n1) = Pbg . (n1 + 1) by A82, A52, A56, A49, A143, GLIB_001:33;

A146: m1 in NAT by ORDINAL1:def 12;

A147: m1 < n1 by A93, A141, A144, XREAL_1:6;

then m1 < len Pbg by A143, XXREAL_0:2;

then A148: (Pag .append Pbg) . ((len Pag) + m1) = Pbg . (m1 + 1) by A82, A52, A56, A49, A146, GLIB_001:33;

reconsider n1 = n1, m1 = m1 as even Element of NAT by A141, A144, ORDINAL1:def 12;

reconsider m11 = m1 + 1, n11 = n1 + 1 as odd Element of NAT ;

A149: m11 < n11 by A147, XREAL_1:6;

n11 <= len Pbg by A143, NAT_1:13;

then A150: m11 < len Pbg by A149, XXREAL_0:2;

then Pbg is chordal by A60, A91, A141, A144, A145, A148, A151, Th84;

then Pb is chordal by A31, Th86;

hence contradiction by A46, Th88; :: thesis: verum

end;A141: m = (len Pag) + m1 by NAT_1:10;

n > len Pag by A93, A140, XXREAL_0:2;

then A142: not n in dom Pag by FINSEQ_3:25;

n in dom (Pag .append Pbg) by A89, A98, FINSEQ_3:25;

then consider n1 being Element of NAT such that

A143: n1 < len Pbg and

A144: n = (len Pag) + n1 by A142, GLIB_001:34;

A145: (Pag .append Pbg) . ((len Pag) + n1) = Pbg . (n1 + 1) by A82, A52, A56, A49, A143, GLIB_001:33;

A146: m1 in NAT by ORDINAL1:def 12;

A147: m1 < n1 by A93, A141, A144, XREAL_1:6;

then m1 < len Pbg by A143, XXREAL_0:2;

then A148: (Pag .append Pbg) . ((len Pag) + m1) = Pbg . (m1 + 1) by A82, A52, A56, A49, A146, GLIB_001:33;

reconsider n1 = n1, m1 = m1 as even Element of NAT by A141, A144, ORDINAL1:def 12;

reconsider m11 = m1 + 1, n11 = n1 + 1 as odd Element of NAT ;

A149: m11 < n11 by A147, XREAL_1:6;

n11 <= len Pbg by A143, NAT_1:13;

then A150: m11 < len Pbg by A149, XXREAL_0:2;

A151: now :: thesis: not m11 + 2 >= n11

n11 <= len Pbg
by A143, NAT_1:13;assume A152:
m11 + 2 >= n11
; :: thesis: contradiction

end;per cases
( m11 + 2 = n11 or m11 + 2 > n11 )
by A152, XXREAL_0:1;

end;

suppose A153:
m11 + 2 = n11
; :: thesis: contradiction

then
m11 + 1 < len Pbg
by A143;

then m11 < (len Pbg) - 1 by XREAL_1:20;

then A154: (len Pag) + m11 < ((len Pbg) - 1) + (len Pag) by XREAL_1:6;

A155: 1 <= (len Pag) + m11 by ABIAN:12, NAT_1:12;

A156: Pbg . (m11 + 1) Joins Pbg . m11,Pbg . n11,G by A150, A153, GLIB_001:def 3;

Pbg . (m11 + 1) = (Pag .append Pbg) . ((len Pag) + m11) by A82, A52, A56, A49, A150, GLIB_001:33;

then Pbg . (m11 + 1) in (Pag .append Pbg) .edges() by A83, A155, A154, GLIB_001:99;

hence contradiction by A92, A141, A144, A145, A148, A156; :: thesis: verum

end;then m11 < (len Pbg) - 1 by XREAL_1:20;

then A154: (len Pag) + m11 < ((len Pbg) - 1) + (len Pag) by XREAL_1:6;

A155: 1 <= (len Pag) + m11 by ABIAN:12, NAT_1:12;

A156: Pbg . (m11 + 1) Joins Pbg . m11,Pbg . n11,G by A150, A153, GLIB_001:def 3;

Pbg . (m11 + 1) = (Pag .append Pbg) . ((len Pag) + m11) by A82, A52, A56, A49, A150, GLIB_001:33;

then Pbg . (m11 + 1) in (Pag .append Pbg) .edges() by A83, A155, A154, GLIB_001:99;

hence contradiction by A92, A141, A144, A145, A148, A156; :: thesis: verum

then Pbg is chordal by A60, A91, A141, A144, A145, A148, A151, Th84;

then Pb is chordal by A31, Th86;

hence contradiction by A46, Th88; :: thesis: verum