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;
now :: thesis: for x being object st x in A holds
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;
then A16: A c= (the_Vertices_of G) \ 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 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
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;
then A24: B c= (the_Vertices_of G) \ 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 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: 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
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;
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;
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;
suppose ( ( a1 = x & a2 = y ) or ( a1 = y & a2 = x ) ) ; :: thesis: contradiction
hence contradiction by A61, A70, Def3; :: thesis: verum
end;
end;
end;
A80: Pag .first() = Pag . 1 ;
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
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;
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 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 ) ;
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;
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;
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;
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 A63, A52, A111, TARSKI:def 2;
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 A113, XXREAL_0:1;
end;
end;
then Pag is chordal by A97, A95, A102, A104, A107, A108, A112, Th84, JORDAN12:2;
then Pa is chordal by A36, Th86;
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 A119, XXREAL_0:1;
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;
end;
end;
then Pag is chordal by A97, A91, A104, A107, A108, A118, Th84;
then Pa is chordal by A36, Th86;
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 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;
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 ;
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 A131, XXREAL_0:1;
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;
end;
end;
then Pbg is chordal by A60, A95, A104, A107, A108, A130, Th84;
then Pb is chordal by A31, Th86;
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 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;
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 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
assume A152: m11 + 2 >= n11 ; :: thesis: contradiction
per cases ( m11 + 2 = n11 or m11 + 2 > n11 ) by A152, XXREAL_0:1;
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;
end;
end;
n11 <= len Pbg by A143, NAT_1:13;
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;
end;