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 () 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
reconsider xg = x, yg = y as Vertex of G by GLIB_000:42;
A12: S = the_Vertices_of Gs by ;
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 () \ S
let x be object ; :: thesis: ( x in A implies x in () \ S )
assume A15: x in A ; :: thesis: x in () \ S
not x in S by ;
hence x in () \ S by ; :: thesis: verum
end;
then A16: A c= () \ S ;
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 ;
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 () 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 ;
A22: not y in {x} by ;
now :: thesis: for x being object st x in B holds
x in () \ S
let x be object ; :: thesis: ( x in B implies x in () \ S )
assume A23: x in B ; :: thesis: x in () \ S
not x in S by ;
hence x in () \ S by ; :: thesis: verum
end;
then A24: B c= () \ S ;
then reconsider Gb = the inducedSubgraph of the removeVertices of G,S,( the removeVertices of G,S .reachableFrom sb) as inducedSubgraph of G,B by ;
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 ;
then x in G .AdjacentSet () by ;
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 ;
A33: ybg in B \/ {xg} by ;
not y in B by ;
then not yg in the_Vertices_of the inducedSubgraph of G,(B \/ {xg}) by ;
then y in G .AdjacentSet (the_Vertices_of the inducedSubgraph of G,(B \/ {xg})) by ;
then the inducedSubgraph of G,((B \/ {x}) \/ {y}) is connected by ;
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 ;
then x in G .AdjacentSet () by ;
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 ;
A38: not y in {x} by ;
not y in A by ;
then not yg in the_Vertices_of the inducedSubgraph of G,(A \/ {xg}) by ;
then y in G .AdjacentSet (the_Vertices_of the inducedSubgraph of G,(A \/ {xg})) by ;
then the inducedSubgraph of G,((A \/ {x}) \/ {y}) is connected by ;
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 ;
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 ;
set P = Pag .append Pbg;
A52: Pag . (len Pag) = yg by ;
A53: Pbg . (len Pbg) = xg by ;
A54: Pbg .last() = Pbg . (len Pbg) ;
then A55: x in Pbg .vertices() by ;
A56: Pbg .first() = Pbg . 1 ;
then A57: y in Pbg .vertices() by ;
A58: not Pbg is trivial by ;
A59: Pbg is open by ;
A60: not Pbg is Cycle-like by ;
A61: not xg,yg are_adjacent by ;
then A62: Pbg .length() >= 2 by A10, A56, A54, A49, A53, Th45;
A63: Pag . 1 = xg by ;
A64: Pag .edges() misses Pbg .edges()
proof
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 ;
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 ;
e in Pbg .edges() by ;
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 ;
e Joins b1,b2,G by ;
then A73: ( ( a1 = b1 & a2 = b2 ) or ( a1 = b2 & a2 = b1 ) ) by A70;
then A74: ( a1 in B or a1 in {xg,yg} ) by ;
A75: the_Vertices_of the inducedSubgraph of G,((A \/ {x}) \/ {y}) = A \/ {xg,yg} by ;
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 ;
A78: ( a2 in B or a2 in {xg,yg} ) by ;
per cases ( ( a1 = x & a2 = x ) or ( a1 = y & a2 = y ) or ( a1 = x & a2 = y ) or ( a1 = y & a2 = x ) ) by ;
suppose A79: ( ( a1 = x & a2 = x ) or ( a1 = y & a2 = y ) ) ; :: thesis: contradiction
end;
suppose ( ( a1 = x & a2 = y ) or ( a1 = y & a2 = x ) ) ; :: thesis: contradiction
end;
end;
end;
A80: Pag .first() = Pag . 1 ;
then A81: x in Pag .vertices() by ;
A82: Pag .last() = Pag . (len Pag) ;
then A83: (len (Pag .append Pbg)) + 1 = (len Pag) + (len Pbg) by ;
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 ;
then (Pag .append Pbg) .length() >= 3 + 1 ;
then A85: (Pag .append Pbg) .length() > 3 by NAT_1:13;
A86: Pag is open by ;
A87: y in Pag .vertices() by ;
{xg,yg} c= (Pag .vertices()) /\ (Pbg .vertices())
proof
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 ; :: thesis: verum
end;
then (Pag .vertices()) /\ (Pbg .vertices()) = {xg,yg} by A51;
then Pag .append Pbg is Cycle-like by A63, A52, A86, A49, A53, A59, A58, A64, Th27;
then Pag .append Pbg is chordal by ;
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 ;
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 ;
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 ) ;
suppose A100: ( m < len Pag & n <= len Pag ) ; :: thesis: contradiction
end;
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 ;
m in dom Pag by ;
then A104: (Pag .append Pbg) . m = Pag . m by GLIB_001:32;
A105: not n in dom Pag by ;
n in dom (Pag .append Pbg) by ;
then consider n1 being Element of NAT such that
A106: n1 < len Pbg and
A107: n = (len Pag) + n1 by ;
A108: (Pag .append Pbg) . ((len Pag) + n1) = Pbg . (n1 + 1) by ;
reconsider n1 = n1 as even Element of NAT by A107;
reconsider n11 = n1 + 1 as odd Element of NAT ;
A109: n11 <= len Pbg by ;
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 ;
suppose A111: ( Pag . m in A & Pbg . n11 in {xg,yg} ) ; :: thesis: contradiction
per cases ( Pbg . n11 = Pag . 1 or Pbg . n11 = Pag . (len Pag) ) by ;
suppose A112: Pbg . n11 = Pag . 1 ; :: thesis: contradiction
now :: thesis: not 1 + 2 >= m
assume A113: 1 + 2 >= m ; :: thesis: contradiction
per cases ( 1 + 2 > m or 1 + 2 = m ) by ;
suppose A114: 1 + 2 = m ; :: thesis: contradiction
then A115: 1 + 1 < len Pag by ;
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 ;
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 ;
1 < len Pag by ;
then Pag . (1 + 1) Joins Pag . 1,Pag . m,G by ;
hence contradiction by A92, A104, A107, A108, A112, A116, A117, GLIB_000:14; :: thesis: verum
end;
end;
end;
then Pag is chordal by ;
then Pa is chordal by ;
hence contradiction by A48, Th88; :: thesis: verum
end;
suppose A118: Pbg . n11 = Pag . (len Pag) ; :: thesis: contradiction
now :: thesis: not m + 2 >= len Pag
set L = len Pag;
assume A119: m + 2 >= len Pag ; :: thesis: contradiction
per cases ( m + 2 = len Pag or m + 2 > len Pag ) by ;
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 ;
then A123: Pag . (m + 1) = (Pag .append Pbg) . (m + 1) by GLIB_001:32;
m < (len Pag) - 1 by ;
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 ;
m < len Pag by ;
then Pag . (m + 1) Joins Pag . m,Pag . (len Pag),G by ;
hence contradiction by A92, A104, A107, A108, A118, A123, A124; :: thesis: verum
end;
end;
end;
then Pag is chordal by ;
then Pa is chordal by ;
hence contradiction by A48, Th88; :: thesis: verum
end;
end;
end;
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 ;
set WAB = the removeVertices of G,S .walkOf (ac,e,bc);
e Joins ac,bc, the removeVertices of G,S by ;
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 ;
then (WAs .append ( the removeVertices of G,S .walkOf (ac,e,bc))) .append WBs is_Walk_from a,b by ;
hence contradiction by A1, A2, Def8; :: thesis: verum
end;
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
.= Pbg . (len Pbg) by ;
now :: thesis: not n11 + 2 >= len Pbg
set L = len Pbg;
assume A131: n11 + 2 >= len Pbg ; :: thesis: contradiction
per cases ( n11 + 2 = len Pbg or n11 + 2 > len Pbg ) by ;
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 ;
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 ;
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 ;
Pbg . (n11 + 1) = (Pag .append Pbg) . ((len Pag) + n11) by ;
then Pbg . (n11 + 1) in (Pag .append Pbg) .edges() by ;
hence contradiction by A92, A104, A107, A108, A130, A136; :: thesis: verum
end;
end;
end;
then Pbg is chordal by ;
then Pb is chordal by ;
hence contradiction by A46, Th88; :: thesis: verum
end;
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 ;
hence contradiction by A4, A11, Th44; :: thesis: verum
end;
end;
end;
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 ;
then A142: not n in dom Pag by FINSEQ_3:25;
n in dom (Pag .append Pbg) by ;
then consider n1 being Element of NAT such that
A143: n1 < len Pbg and
A144: n = (len Pag) + n1 by ;
A145: (Pag .append Pbg) . ((len Pag) + n1) = Pbg . (n1 + 1) by ;
A146: m1 in NAT by ORDINAL1:def 12;
A147: m1 < n1 by ;
then m1 < len Pbg by ;
then A148: (Pag .append Pbg) . ((len Pag) + m1) = Pbg . (m1 + 1) by ;
reconsider n1 = n1, m1 = m1 as even Element of NAT by ;
reconsider m11 = m1 + 1, n11 = n1 + 1 as odd Element of NAT ;
A149: m11 < n11 by ;
n11 <= len Pbg by ;
then A150: m11 < len Pbg by ;
A151: now :: thesis: not m11 + 2 >= n11
assume A152: m11 + 2 >= n11 ; :: thesis: contradiction
per cases ( m11 + 2 = n11 or m11 + 2 > n11 ) by ;
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 ;
A156: Pbg . (m11 + 1) Joins Pbg . m11,Pbg . n11,G by ;
Pbg . (m11 + 1) = (Pag .append Pbg) . ((len Pag) + m11) by ;
then Pbg . (m11 + 1) in (Pag .append Pbg) .edges() by ;
hence contradiction by A92, A141, A144, A145, A148, A156; :: thesis: verum
end;
end;
end;
n11 <= len Pbg by ;
then Pbg is chordal by ;
then Pb is chordal by ;
hence contradiction by A46, Th88; :: thesis: verum
end;
end;