let G be chordal _Graph; :: thesis:
set tVG = the_Vertices_of G;
let a, b be Vertex of G; :: thesis:
assume that
A1: a <> b and
A2: not a,b are_adjacent ; :: thesis:
let S be VertexSeparator of a,b; :: thesis:
assume that
A3: S is minimal and
A4: not S is empty ; :: thesis:
let Gs be inducedSubgraph of G,S; :: thesis:
consider Gns being removeVertices of G,S;
reconsider sa = a, sb = b as Vertex of Gns by A1, A2, Th77;
set A = Gns .reachableFrom sa;
set B = Gns .reachableFrom sb;
A5: S is VertexSeparator of b,a by A1, A2, Th70;
A6: (Gns .reachableFrom sa) /\ (Gns .reachableFrom sb) = {} by A1, A2, Th76;
A7: ( (Gns .reachableFrom sa) /\ S = {} & (Gns .reachableFrom sb) /\ S = {} ) by A1, A2, A5, Th75;
consider Ga being inducedSubgraph of Gns,(Gns .reachableFrom sa);
consider Gb being inducedSubgraph of Gns,(Gns .reachableFrom sb);
A8: the_Vertices_of Ga = Gns .reachableFrom sa by GLIB_000:def 39;
A9: the_Vertices_of Gb = Gns .reachableFrom sb by GLIB_000:def 39;
the_Vertices_of Gns c= the_Vertices_of G ;
then reconsider A = Gns .reachableFrom sa, B = Gns .reachableFrom sb as non empty Subset of (the_Vertices_of G) by XBOOLE_1:1;
not a in S by A1, A2, Def8;
then A10: (the_Vertices_of G) \ S is non empty Subset of (the_Vertices_of G) by XBOOLE_0:def 5;

now

let x be set ; :: thesis:
assume A11: x in A ; :: thesis:
not x in S by A7, A11, XBOOLE_0:def 4;
hence x in (the_Vertices_of G) \ S by A11, XBOOLE_0:def 5; :: thesis:

end;

then A12: A c= (the_Vertices_of G) \ S by TARSKI:def 3;

now

let x be set ; :: thesis:
assume A13: x in B ; :: thesis:
not x in S by A7, A13, XBOOLE_0:def 4;
hence x in (the_Vertices_of G) \ S by A13, XBOOLE_0:def 5; :: thesis:

end;

then A14: B c= (the_Vertices_of G) \ S by TARSKI:def 3;
reconsider Ga = Ga as inducedSubgraph of G,A by A10, A12, Th29;
reconsider Gb = Gb as inducedSubgraph of G,B by A10, A14, Th29;
let x, y be Vertex of Gs; :: according to CHORD:def 6 :: thesis:
assume that
A15: x <> y and
A16: not x,y are_adjacent ; :: thesis:
reconsider xg = x, yg = y as Vertex of G by GLIB_000:45;
A17: S = the_Vertices_of Gs by A4, GLIB_000:def 39;
A18: not xg,yg are_adjacent by A4, A16, Th45;
set xy = {xg,yg};
set Bx = B \/ {xg};
set Ax = A \/ {xg};
consider Gax being inducedSubgraph of G,(A \/ {xg});
A19: the_Vertices_of Gax = A \/ {xg} by GLIB_000:def 39;
consider Ga1 being inducedSubgraph of G,((A \/ {x}) \/ {y});
A20: (A \/ {x}) \/ {y} = A \/ ({x} \/ {y}) by XBOOLE_1:4
.= A \/ {xg,yg} by ENUMSET1:41 ;
then A21: the_Vertices_of Ga1 c= A \/ {xg,yg} by GLIB_000:def 39;
( x in {xg,yg} & y in {xg,yg} ) by TARSKI:def 2;
then ( x in A \/ {xg,yg} & y in A \/ {xg,yg} ) by XBOOLE_0:def 3;
then reconsider xa = x, ya = y as Vertex of Ga1 by A20, GLIB_000:def 39;
consider xag being Vertex of G such that
A22: xag in A and
A23: xg,xag are_adjacent by A1, A2, A3, A17, Th82;
not x in A by A12, A17, XBOOLE_0:def 5;
then x in G .AdjacentSet (the_Vertices_of Ga) by A8, A22, A23;
then A24: Gax is connected by Th57;
consider yag being Vertex of G such that
A25: yag in A and
A26: yg,yag are_adjacent by A1, A2, A3, A17, Th82;
A27: yag in A \/ {xg} by A25, XBOOLE_0:def 3;
( not y in A & not y in {x} ) by A12, A15, A17, TARSKI:def 1, XBOOLE_0:def 5;
then not yg in the_Vertices_of Gax by A19, XBOOLE_0:def 3;
then y in G .AdjacentSet (the_Vertices_of Gax) by A19, A26, A27;
then Ga1 is connected by A24, Th57;
then consider Wa being Walk of Ga1 such that
A28: Wa is_Walk_from xa,ya by GLIB_002:def 1;
A29: ( Wa .first() = xa & Wa .last() = ya ) by A28, GLIB_001:def 23;
consider Pa being Path of Ga1 such that
A30: Pa is_Walk_from Wa .first() ,Wa .last() and
A31: Pa is minlength by Th39;
consider Gbx being inducedSubgraph of G,(B \/ {xg});
A32: the_Vertices_of Gbx = B \/ {xg} by GLIB_000:def 39;
consider Gb1 being inducedSubgraph of G,((B \/ {x}) \/ {y});
A33: (B \/ {x}) \/ {y} = B \/ ({x} \/ {y}) by XBOOLE_1:4
.= B \/ {xg,yg} by ENUMSET1:41 ;
then A34: the_Vertices_of Gb1 c= B \/ {xg,yg} by GLIB_000:def 39;
( x in {xg,yg} & y in {xg,yg} ) by TARSKI:def 2;
then ( x in B \/ {xg,yg} & y in B \/ {xg,yg} ) by XBOOLE_0:def 3;
then reconsider xb = x, yb = y as Vertex of Gb1 by A33, GLIB_000:def 39;
consider xbg being Vertex of G such that
A35: xbg in B and
A36: xg,xbg are_adjacent by A1, A2, A3, A17, Th83;
not x in B by A14, A17, XBOOLE_0:def 5;
then x in G .AdjacentSet (the_Vertices_of Gb) by A9, A35, A36;
then A37: Gbx is connected by Th57;
consider ybg being Vertex of G such that
A38: ybg in B and
A39: yg,ybg are_adjacent by A1, A2, A3, A17, Th83;
A40: ybg in B \/ {xg} by A38, XBOOLE_0:def 3;
( not y in B & not y in {x} ) by A14, A15, A17, TARSKI:def 1, XBOOLE_0:def 5;
then not yg in the_Vertices_of Gbx by A32, XBOOLE_0:def 3;
then y in G .AdjacentSet (the_Vertices_of Gbx) by A32, A39, A40;
then Gb1 is connected by A37, Th57;
then consider Wb being Walk of Gb1 such that
A41: Wb is_Walk_from yb,xb by GLIB_002:def 1;
A42: ( Wb .first() = ya & Wb .last() = xa ) by A41, GLIB_001:def 23;
consider Pb being Path of Gb1 such that
A43: Pb is_Walk_from Wb .first() ,Wb .last() and
A44: Pb is minlength by Th39;
reconsider Pag = Pa, Pbg = Pb as Path of G by GLIB_001:176;
A45: ( Pag .first() = Pag . 1 & Pag .last() = Pag . (len Pag) ) ;
( Pa .first() = Pa . 1 & Pa .last() = Pa . (len Pa) ) ;
then A46: ( Pag . 1 = xg & Pag . (len Pag) = yg ) by A29, A30, GLIB_001:def 23;
then A47: not Pag is closed by A15, A45, GLIB_001:def 24;
then A48: not Pag is Cycle-like ;
A49: ( x in Pag .vertices() & y in Pag .vertices() ) by A45, A46, GLIB_001:89;
A50: ( Pbg .first() = Pbg . 1 & Pbg .last() = Pbg . (len Pbg) ) ;
A51: ( Pb .first() = Pb . 1 & Pb .last() = Pb . (len Pb) ) ;
then A52: ( Pbg . 1 = yg & Pbg . (len Pbg) = xg ) by A42, A43, GLIB_001:def 23;
then A53: not Pbg is closed by A15, A50, GLIB_001:def 24;
then A54: not Pbg is Cycle-like ;
A55: ( x in Pbg .vertices() & y in Pbg .vertices() ) by A50, A52, GLIB_001:89;
set P = Pag .append Pbg;
A56: (len (Pag .append Pbg)) + 1 = (len Pag) + (len Pbg) by A45, A46, A50, A52, GLIB_001:29;
A57: not Pag is trivial by A15, A45, A46, GLIB_001:128;
A58: Pag .length() >= 2 by A15, A18, A45, A46, Th46;
A59: not Pbg is trivial by A15, A50, A52, GLIB_001:128;
A60: Pbg .length() >= 2 by A15, A18, A50, A52, Th46;
A61: (Pag .vertices() ) /\ (Pbg .vertices() ) = {xg,yg}

proof

thus (Pag .vertices() ) /\ (Pbg .vertices() ) c= {xg,yg} :: according to XBOOLE_0:def 10 :: thesis:

proof

Pag .vertices() = Pa .vertices() by GLIB_001:99;
then A62: Pag .vertices() c= A \/ {xg,yg} by A21, XBOOLE_1:1;
Pbg .vertices() = Pb .vertices() by GLIB_001:99;
then A63: Pbg .vertices() c= B \/ {xg,yg} by A34, XBOOLE_1:1;
(A \/ {xg,yg}) /\ (B \/ {xg,yg}) = (A /\ B) \/ {xg,yg} by XBOOLE_1:24
.= {xg,yg} by A6 ;
hence (Pag .vertices() ) /\ (Pbg .vertices() ) c= {xg,yg} by A62, A63, XBOOLE_1:27; :: thesis:

end;

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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {xg,yg} ; :: thesis:
then ( a = x or a = y ) by TARSKI:def 2;
hence a in (Pag .vertices() ) /\ (Pbg .vertices() ) by A49, A55, XBOOLE_0:def 4; :: thesis:

end;

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

proof

assume (Pag .edges() ) /\ (Pbg .edges() ) <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
then consider e being set 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 A66: e in Pa .edges() by GLIB_001:111;
e in Pbg .edges() by A65, XBOOLE_0:def 4;
then A67: e in Pb .edges() by GLIB_001:111;
consider a1, a2 being Vertex of Ga1, na being odd Element of NAT such that
A68: na + 2 <= len Pag and
A69: a1 = Pag . na and
e = Pag . (na + 1) and
A70: a2 = Pag . (na + 2) and
A71: e Joins a1,a2,Ga1 by A66, GLIB_001:104;
consider b1, b2 being Vertex of Gb1, 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
A72: e Joins b1,b2,Gb1 by A67, GLIB_001:104;
A73: ( e Joins a1,a2,G & e Joins b1,b2,G ) by A71, A72, GLIB_000:75;
then A74: ( ( a1 = b1 & a2 = b2 ) or ( a1 = b2 & a2 = b1 ) ) by GLIB_000:18;
the_Vertices_of Ga1 = A \/ {xg,yg} by A20, GLIB_000:def 39;
then A75: ( ( a1 in A or a1 in {xg,yg} ) & ( a2 in A or a2 in {xg,yg} ) ) by XBOOLE_0:def 3;
the_Vertices_of Gb1 = B \/ {xg,yg} by A33, GLIB_000:def 39;
then A76: ( ( a1 in B or a1 in {xg,yg} ) & ( a2 in B or a2 in {xg,yg} ) ) by A74, XBOOLE_0:def 3;

per cases by A6, A75, A76, TARSKI:def 2, XBOOLE_0:def 4;

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

na < na + 2 by XREAL_1:41;
hence contradiction by A15, A46, A68, A69, A70, A77, GLIB_001:def 28; :: thesis:

end;

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

hence contradiction by A18, A73, Def3; :: thesis:

end;

(Pag .append Pbg) .length() = (Pag .length() ) + (Pbg .length() ) by A45, A46, A50, A52, Th28;
then (Pag .append Pbg) .length() >= 2 + 2 by A58, A60, XREAL_1:9;
then (Pag .append Pbg) .length() >= 3 + 1 ;
then A78: (Pag .append Pbg) .length() > 3 by NAT_1:13;
Pag .append Pbg is Cycle-like by A45, A46, A47, A50, A52, A53, A57, A59, A61, A64, Th27;
then Pag .append Pbg is chordal by A78, Def11;
then consider m, n being odd Nat such that
A79: m + 2 < n and
A80: n <= len (Pag .append Pbg) and
A81: (Pag .append Pbg) . m <> (Pag .append Pbg) . n and
A82: ex e being set st e Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G and
A83: for f being set st f in (Pag .append Pbg) .edges() holds
not f Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G by Def10;
A84: ( m in NAT & n in NAT ) by ORDINAL1:def 13;
A85: m < n by A79, NAT_1:12;
consider e being set such that
A86: e Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G by A82;
A87: e Joins (Pag .append Pbg) . n,(Pag .append Pbg) . m,G by A86, GLIB_000:17;
A88: 1 <= m by HEYTING3:1;
A89: 1 <= n by HEYTING3:1;

per cases ;

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

then ( m in dom Pag & n in dom Pag ) by A88, A89, FINSEQ_3:27;
then ( (Pag .append Pbg) . m = Pag . m & (Pag .append Pbg) . n = Pag . n ) by GLIB_001:33;
then Pag is chordal by A48, A79, A82, A90, Th85;
then Pa is chordal by A20, Th87;
hence contradiction by A31, Th89; :: thesis:

end;

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

then m in dom Pag by A88, FINSEQ_3:27;
then A92: (Pag .append Pbg) . m = Pag . m by GLIB_001:33;
( n in dom (Pag .append Pbg) & not n in dom Pag ) by A80, A89, A91, FINSEQ_3:27;
then consider n1 being Element of NAT such that
A93: n1 < len Pbg and
A94: n = (len Pag) + n1 by GLIB_001:35;
A95: (Pag .append Pbg) . ((len Pag) + n1) = Pbg . (n1 + 1) by A45, A46, A50, A52, A93, GLIB_001:34;
A96: Pag . m in the_Vertices_of Ga1 by A84, A91, GLIB_001:8;
n1 - 0 = n - (len Pag) by A94;
then reconsider n1 = n1 as even Element of NAT ;
reconsider n11 = n1 + 1 as odd Element of NAT ;
A97: n11 <= len Pbg by A93, NAT_1:13;
then A98: Pbg . n11 in the_Vertices_of Gb1 by GLIB_001:8;

per cases by A21, A34, A96, A98, XBOOLE_0:def 3;

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

per cases by A46, A99, TARSKI:def 2;

suppose A100: Pbg . n11 = Pag . 1 ; :: thesis:

now

assume A101: 1 + 2 >= m ; :: thesis:

per cases by A101, XXREAL_0:1;

suppose 1 + 2 > m ; :: thesis:

then 1 >= m by Th4, JORDAN12:3;
hence contradiction by A81, A88, A92, A94, A95, A100, XXREAL_0:1; :: thesis:

end;

suppose A102: 1 + 2 = m ; :: thesis:

1 < len Pag by A88, A91, XXREAL_0:2;
then A103: Pag . (1 + 1) Joins Pag . 1,Pag . m,G by A102, GLIB_001:def 3, JORDAN12:3;
A104: 1 + 1 < len Pag by A91, A102, XXREAL_0:2;
then 1 + 1 in dom Pag by FINSEQ_3:27;
then A105: Pag . (1 + 1) = (Pag .append Pbg) . (1 + 1) by GLIB_001:33;
1 < (len Pag) - 1 by A104, XREAL_1:22;
then 1 + 0 < ((len Pag) - 1) + (len Pbg) by XREAL_1:10;
then (Pag .append Pbg) . (1 + 1) in (Pag .append Pbg) .edges() by A56, GLIB_001:101, JORDAN12:3;
hence contradiction by A83, A92, A94, A95, A100, A103, A105, GLIB_000:17; :: thesis:

end;

then Pag is chordal by A48, A87, A91, A92, A94, A95, A100, Th85, JORDAN12:3;
then Pa is chordal by A20, Th87;
hence contradiction by A31, Th89; :: thesis:

end;

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

now

assume A107: m + 2 >= len Pag ; :: thesis:
set L = len Pag;

per cases by A107, XXREAL_0:1;

suppose A108: m + 2 = len Pag ; :: thesis:

then A109: len Pag = (m + 1) + 1 ;
then A110: m + 1 < len Pag by NAT_1:13;
then m < len Pag by NAT_1:13;
then A111: Pag . (m + 1) Joins Pag . m,Pag . (len Pag),G by A84, A108, GLIB_001:def 3;
1 <= m + 1 by NAT_1:12;
then m + 1 in dom Pag by A110, FINSEQ_3:27;
then A112: Pag . (m + 1) = (Pag .append Pbg) . (m + 1) by GLIB_001:33;
m < (len Pag) - 1 by A109, NAT_1:13;
then m + 0 < ((len Pag) - 1) + (len Pbg) by XREAL_1:10;
then (Pag .append Pbg) . (m + 1) in (Pag .append Pbg) .edges() by A56, GLIB_001:101;
hence contradiction by A83, A92, A94, A95, A106, A111, A112; :: thesis:

end;

suppose m + 2 > len Pag ; :: thesis:

hence contradiction by A91, Th4; :: thesis:

end;

then Pag is chordal by A48, A82, A92, A94, A95, A106, Th85;
then Pa is chordal by A20, Th87;
hence contradiction by A31, Th89; :: thesis:

end;

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

then reconsider ac = Pa . m as Vertex of Ga by GLIB_000:def 39;
a in A by GLIB_002:9;
then reconsider aa = a as Vertex of Ga by GLIB_000:def 39;
reconsider bc = Pb . n11 as Vertex of Gb by A113, GLIB_000:def 39;
b in B by GLIB_002:9;
then reconsider bb = b as Vertex of Gb by GLIB_000:def 39;
consider WA being Walk of Ga such that
A114: WA is_Walk_from aa,ac by GLIB_002:def 1;
consider WB being Walk of Gb such that
A115: WB is_Walk_from bc,bb by GLIB_002:def 1;
reconsider WA = WA, WB = WB as Walk of Gns by GLIB_001:168;
set WAB = Gns .walkOf ac,e,bc;
e Joins ac,bc,Gns by A12, A14, A86, A92, A94, A95, A113, Th19;
then A116: Gns .walkOf ac,e,bc is_Walk_from ac,bc by GLIB_001:16;
reconsider WAs = WA, WBs = WB as Walk of Gns ;
set WaB = WAs .append (Gns .walkOf ac,e,bc);
set Wab = (WAs .append (Gns .walkOf ac,e,bc)) .append WBs;
WAs is_Walk_from aa,ac by A114, GLIB_001:20;
then A117: WAs .append (Gns .walkOf ac,e,bc) is_Walk_from aa,bc by A116, GLIB_001:32;
WBs is_Walk_from bc,bb by A115, GLIB_001:20;
then (WAs .append (Gns .walkOf ac,e,bc)) .append WBs is_Walk_from a,b by A117, GLIB_001:32;
hence contradiction by A1, A2, Def8; :: thesis:

end;

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

then ( Pag . m = x or Pag . m = y ) by TARSKI:def 2;
then A118: Pag . m = x by A46, A84, A91, GLIB_001:def 28
.= Pbg . (len Pbg) by A42, A43, A51, GLIB_001:def 23 ;

now

assume A119: n11 + 2 >= len Pbg ; :: thesis:
set L = len Pbg;

per cases by A119, XXREAL_0:1;

suppose A120: n11 + 2 = len Pbg ; :: thesis:

then A121: len Pbg = (n11 + 1) + 1 ;
then n11 + 1 < len Pbg by NAT_1:13;
then A122: n11 < len Pbg by NAT_1:13;
then Pbg . (n11 + 1) Joins Pbg . n11,Pbg . (len Pbg),Gb1 by A120, GLIB_001:def 3;
then Pbg . (n11 + 1) Joins Pbg . (len Pbg),Pbg . n11,Gb1 by GLIB_000:17;
then A123: Pbg . (n11 + 1) Joins Pbg . (len Pbg),Pbg . n11,G by GLIB_000:75;
A124: Pbg . (n11 + 1) = (Pag .append Pbg) . ((len Pag) + n11) by A45, A46, A50, A52, A122, GLIB_001:34;
A125: 1 <= (len Pag) + n11 by HEYTING3:1, NAT_1:12;
n11 < (len Pbg) - 1 by A121, NAT_1:13;
then (len Pag) + n11 < ((len Pbg) - 1) + (len Pag) by XREAL_1:8;
then Pbg . (n11 + 1) in (Pag .append Pbg) .edges() by A56, A124, A125, GLIB_001:100;
hence contradiction by A83, A92, A94, A95, A118, A123; :: thesis:

end;

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

then n11 >= len Pbg by Th4;
hence contradiction by A81, A92, A94, A95, A97, A118, XXREAL_0:1; :: thesis:

end;

then Pbg is chordal by A54, A87, A92, A94, A95, A118, Th85;
then Pb is chordal by A33, Th87;
hence contradiction by A44, Th89; :: thesis:

end;

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

then ( ( Pag . m = x or Pag . m = y ) & ( Pbg . n11 = x or Pbg . n11 = y ) ) by TARSKI:def 2;
then xg,yg are_adjacent by A81, A82, A92, A94, A95, Def3;
hence contradiction by A4, A16, Th45; :: thesis:

end;

suppose A126: len Pag <= m ; :: thesis:

then consider m1 being Nat such that
A127: m = (len Pag) + m1 by NAT_1:10;
A128: m1 in NAT by ORDINAL1:def 13;
n > len Pag by A85, A126, XXREAL_0:2;
then ( n in dom (Pag .append Pbg) & not n in dom Pag ) by A80, A89, FINSEQ_3:27;
then consider n1 being Element of NAT such that
A129: n1 < len Pbg and
A130: n = (len Pag) + n1 by GLIB_001:35;
A131: (Pag .append Pbg) . ((len Pag) + n1) = Pbg . (n1 + 1) by A45, A46, A50, A52, A129, GLIB_001:34;
A132: m1 < n1 by A85, A127, A130, XREAL_1:8;
then m1 < len Pbg by A129, XXREAL_0:2;
then A133: (Pag .append Pbg) . ((len Pag) + m1) = Pbg . (m1 + 1) by A45, A46, A50, A52, A128, GLIB_001:34;
( n1 - 0 = n - (len Pag) & m1 - 0 = m - (len Pag) ) by A127, A130;
then reconsider n1 = n1, m1 = m1 as even Element of NAT by ORDINAL1:def 13;
reconsider m11 = m1 + 1, n11 = n1 + 1 as odd Element of NAT ;
A134: n11 <= len Pbg by A129, NAT_1:13;
m11 < n11 by A132, XREAL_1:8;
then A135: m11 < len Pbg by A134, XXREAL_0:2;

A136: now

assume A137: m11 + 2 >= n11 ; :: thesis:

per cases by A137, XXREAL_0:1;

suppose A138: m11 + 2 = n11 ; :: thesis:

then A139: Pbg . (m11 + 1) Joins Pbg . m11,Pbg . n11,G by A135, GLIB_001:def 3;
A140: Pbg . (m11 + 1) = (Pag .append Pbg) . ((len Pag) + m11) by A45, A46, A50, A52, A135, GLIB_001:34;
A141: 1 <= (len Pag) + m11 by HEYTING3:1, NAT_1:12;
m11 + 1 < len Pbg by A129, A138;
then m11 < (len Pbg) - 1 by XREAL_1:22;
then (len Pag) + m11 < ((len Pbg) - 1) + (len Pag) by XREAL_1:8;
then Pbg . (m11 + 1) in (Pag .append Pbg) .edges() by A56, A140, A141, GLIB_001:100;
hence contradiction by A83, A127, A130, A131, A133, A139; :: thesis:

end;

suppose m11 + 2 > n11 ; :: thesis:

then m11 >= n11 by Th4;
hence contradiction by A132, XREAL_1:8; :: thesis:

end;

n11 <= len Pbg by A129, NAT_1:13;
then Pbg is chordal by A54, A82, A127, A130, A131, A133, A136, Th85;
then Pb is chordal by A33, Th87;
hence contradiction by A44, Th89; :: thesis:

end;