let G be chordal _Graph; 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; ( 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
; 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; ( 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
; for H being inducedSubgraph of G,S holds H is complete
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:
(Gns .reachableFrom sa) /\ (Gns .reachableFrom sb) = {}
by A1, A2, Th76;
consider Gb being inducedSubgraph of Gns,(Gns .reachableFrom sb);
consider Ga being inducedSubgraph of Gns,(Gns .reachableFrom sa);
A6:
the_Vertices_of Ga = Gns .reachableFrom sa
by GLIB_000:def 39;
A7:
the_Vertices_of Gb = Gns .reachableFrom sb
by GLIB_000:def 39;
A8:
(Gns .reachableFrom sb) /\ S = {}
by A1, A2, Th75;
A9:
(Gns .reachableFrom sa) /\ S = {}
by A1, A2, Th75;
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;
let Gs be inducedSubgraph of G,S; Gs is complete
let x, y be Vertex of Gs; CHORD:def 6 ( x <> y implies x,y are_adjacent )
assume that
A10:
x <> y
and
A11:
not x,y are_adjacent
; contradiction
reconsider xg = x, yg = y as Vertex of G by GLIB_000:45;
A12:
S = the_Vertices_of Gs
by A4, GLIB_000:def 39;
then A13:
ex xag being Vertex of G st
( xag in A & xg,xag are_adjacent )
by A1, A2, A3, Th82;
set Bx = B \/ {xg};
set Ax = A \/ {xg};
consider Gbx being inducedSubgraph of G,(B \/ {xg});
consider Gax being inducedSubgraph of G,(A \/ {xg});
set xy = {xg,yg};
A14:
the_Vertices_of Gbx = B \/ {xg}
by GLIB_000:def 39;
then A16:
A c= (the_Vertices_of G) \ S
by TARSKI:def 3;
consider yag being Vertex of G such that
A17:
yag in A
and
A18:
yg,yag are_adjacent
by A1, A2, A3, A12, Th82;
A19:
yag in A \/ {xg}
by A17, XBOOLE_0:def 3;
consider Gb1 being inducedSubgraph of G,((B \/ {x}) \/ {y});
consider Ga1 being inducedSubgraph of G,((A \/ {x}) \/ {y});
A20:
the_Vertices_of Gax = A \/ {xg}
by GLIB_000:def 39;
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 = Ga as inducedSubgraph of G,A by A16, Th29;
A22:
not y in {x}
by A10, TARSKI:def 1;
then A24:
B c= (the_Vertices_of G) \ S
by TARSKI:def 3;
then reconsider Gb = Gb 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, Th83;
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:
Gbx is connected
by Th57;
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, Th83;
A31: (B \/ {x}) \/ {y} =
B \/ ({x} \/ {y})
by XBOOLE_1:4
.=
B \/ {xg,yg}
by ENUMSET1:41
;
then A32:
the_Vertices_of Gb1 c= B \/ {xg,yg}
by GLIB_000:def 39;
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 Gb1 by A31, A28, GLIB_000:def 39;
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 Gbx
by A14, A22, XBOOLE_0:def 3;
then
y in G .AdjacentSet (the_Vertices_of Gbx)
by A14, A30, A33;
then
Gb1 is connected
by A27, Th57;
then consider Wb being Walk of Gb1 such that
A34:
Wb is_Walk_from yb,xb
by GLIB_002:def 1;
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:
Gax is connected
by Th57;
A36: (A \/ {x}) \/ {y} =
A \/ ({x} \/ {y})
by XBOOLE_1:4
.=
A \/ {xg,yg}
by ENUMSET1:41
;
then A37:
the_Vertices_of Ga1 c= A \/ {xg,yg}
by GLIB_000:def 39;
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 Ga1 by A36, A25, GLIB_000:def 39;
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 Gax
by A20, A38, XBOOLE_0:def 3;
then
y in G .AdjacentSet (the_Vertices_of Gax)
by A20, A18, A19;
then
Ga1 is connected
by A35, Th57;
then consider Wa being Walk of Ga1 such that
A39:
Wa is_Walk_from xa,ya
by GLIB_002:def 1;
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, GLIB_001:def 23;
A42:
Wa .first() = xa
by A39, GLIB_001:def 23;
A43:
Wb .last() = xa
by A34, GLIB_001:def 23;
A44:
Wb .first() = ya
by A34, GLIB_001:def 23;
consider Pb being Path of Gb1 such that
A45:
Pb is_Walk_from Wb .first() ,Wb .last()
and
A46:
Pb is minlength
by Th39;
consider Pa being Path of Ga1 such that
A47:
Pa is_Walk_from Wa .first() ,Wa .last()
and
A48:
Pa is minlength
by Th39;
reconsider Pag = Pa, Pbg = Pb as Path of G by GLIB_001:176;
Pb .first() = Pb . 1
;
then A49:
Pbg . 1 = yg
by A44, A45, GLIB_001:def 23;
Pbg .vertices() = Pb .vertices()
by GLIB_001:99;
then A50:
Pbg .vertices() c= B \/ {xg,yg}
by A32, XBOOLE_1:1;
Pag .vertices() = Pa .vertices()
by GLIB_001:99;
then
Pag .vertices() c= A \/ {xg,yg}
by A37, XBOOLE_1:1;
then A51:
(Pag .vertices() ) /\ (Pbg .vertices() ) c= {xg,yg}
by A50, A40, XBOOLE_1:27;
set P = Pag .append Pbg;
Pa .last() = Pa . (len Pa)
;
then A52:
Pag . (len Pag) = yg
by A41, A47, GLIB_001:def 23;
A53:
Pb .last() = Pb . (len Pb)
;
then A54:
Pbg . (len Pbg) = xg
by A43, A45, GLIB_001:def 23;
A55:
Pbg .last() = Pbg . (len Pbg)
;
then A56:
x in Pbg .vertices()
by A54, GLIB_001:89;
A57:
Pbg .first() = Pbg . 1
;
then A58:
y in Pbg .vertices()
by A49, GLIB_001:89;
A59:
not Pbg is trivial
by A10, A57, A55, A49, A54, GLIB_001:128;
A60:
not Pbg is closed
by A10, A57, A55, A49, A54, GLIB_001:def 24;
A61:
not Pbg is Cycle-like
by A10, A57, A55, A49, A54, GLIB_001:def 24;
A62:
not xg,yg are_adjacent
by A4, A11, Th45;
then A63:
Pbg .length() >= 2
by A10, A57, A55, A49, A54, Th46;
Pa .first() = Pa . 1
;
then A64:
Pag . 1 = xg
by A42, A47, GLIB_001:def 23;
A65:
Pag .edges() misses Pbg .edges()
proof
assume
(Pag .edges() ) /\ (Pbg .edges() ) <> {}
;
XBOOLE_0:def 7 contradiction
then consider e being
set such that A66:
e in (Pag .edges() ) /\ (Pbg .edges() )
by XBOOLE_0:def 1;
e in Pag .edges()
by A66, XBOOLE_0:def 4;
then
e in Pa .edges()
by GLIB_001:111;
then consider a1,
a2 being
Vertex of
Ga1,
na being
odd Element of
NAT such that A67:
na + 2
<= len Pag
and A68:
a1 = Pag . na
and
e = Pag . (na + 1)
and A69:
a2 = Pag . (na + 2)
and A70:
e Joins a1,
a2,
Ga1
by GLIB_001:104;
A71:
e Joins a1,
a2,
G
by A70, GLIB_000:75;
e in Pbg .edges()
by A66, XBOOLE_0:def 4;
then
e in Pb .edges()
by GLIB_001:111;
then 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 GLIB_001:104;
A73:
the_Vertices_of Gb1 = B \/ {xg,yg}
by A31, GLIB_000:def 39;
e Joins b1,
b2,
G
by A72, GLIB_000:75;
then A74:
( (
a1 = b1 &
a2 = b2 ) or (
a1 = b2 &
a2 = b1 ) )
by A71, GLIB_000:18;
then A75:
(
a1 in B or
a1 in {xg,yg} )
by A73, XBOOLE_0:def 3;
A76:
the_Vertices_of Ga1 = A \/ {xg,yg}
by A36, GLIB_000:def 39;
then A77:
(
a1 in A or
a1 in {xg,yg} )
by XBOOLE_0:def 3;
A78:
(
a2 in A or
a2 in {xg,yg} )
by A76, XBOOLE_0:def 3;
A79:
(
a2 in B or
a2 in {xg,yg} )
by A74, A73, XBOOLE_0:def 3;
end;
A81:
Pag .first() = Pag . 1
;
then A82:
x in Pag .vertices()
by A64, GLIB_001:89;
A83:
Pag .last() = Pag . (len Pag)
;
then A84:
(len (Pag .append Pbg)) + 1 = (len Pag) + (len Pbg)
by A52, A57, A49, GLIB_001:29;
A85:
Pag .length() >= 2
by A10, A62, A81, A83, A64, A52, Th46;
(Pag .append Pbg) .length() = (Pag .length() ) + (Pbg .length() )
by A83, A52, A57, A49, Th28;
then
(Pag .append Pbg) .length() >= 2 + 2
by A85, A63, XREAL_1:9;
then
(Pag .append Pbg) .length() >= 3 + 1
;
then A86:
(Pag .append Pbg) .length() > 3
by NAT_1:13;
A87:
not Pag is closed
by A10, A81, A83, A64, A52, GLIB_001:def 24;
A88:
y in Pag .vertices()
by A83, A52, GLIB_001:89;
{xg,yg} c= (Pag .vertices() ) /\ (Pbg .vertices() )
then
(Pag .vertices() ) /\ (Pbg .vertices() ) = {xg,yg}
by A51, XBOOLE_0:def 10;
then
Pag .append Pbg is Cycle-like
by A81, A83, A64, A52, A87, A57, A55, A49, A54, A60, A59, A65, Th27;
then
Pag .append Pbg is chordal
by A86, Def11;
then consider m, n being odd Nat such that
A89:
m + 2 < n
and
A90:
n <= len (Pag .append Pbg)
and
A91:
(Pag .append Pbg) . m <> (Pag .append Pbg) . n
and
A92:
ex e being set st e Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G
and
A93:
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;
A94:
m < n
by A89, NAT_1:12;
consider e being set such that
A95:
e Joins (Pag .append Pbg) . m,(Pag .append Pbg) . n,G
by A92;
A96:
e Joins (Pag .append Pbg) . n,(Pag .append Pbg) . m,G
by A95, GLIB_000:17;
A97:
m in NAT
by ORDINAL1:def 13;
A98:
not Pag is Cycle-like
by A10, A81, A83, A64, A52, GLIB_001:def 24;
A99:
1 <= n
by HEYTING3:1;
A100:
1 <= m
by HEYTING3:1;
per cases
( ( m < len Pag & n <= len Pag ) or ( m < len Pag & len Pag < n ) or len Pag <= m )
;
suppose A101:
(
m < len Pag &
n <= len Pag )
;
contradictionthen
n in dom Pag
by A99, FINSEQ_3:27;
then A102:
(Pag .append Pbg) . n = Pag . n
by GLIB_001:33;
m in dom Pag
by A100, A101, FINSEQ_3:27;
then
(Pag .append Pbg) . m = Pag . m
by GLIB_001:33;
then
Pag is
chordal
by A98, A89, A92, A101, A102, Th85;
then
Pa is
chordal
by A36, Th87;
hence
contradiction
by A48, Th89;
verum end; suppose A103:
(
m < len Pag &
len Pag < n )
;
contradictionthen A104:
Pag . m in the_Vertices_of Ga1
by A97, GLIB_001:8;
m in dom Pag
by A100, A103, FINSEQ_3:27;
then A105:
(Pag .append Pbg) . m = Pag . m
by GLIB_001:33;
A106:
not
n in dom Pag
by A103, FINSEQ_3:27;
n in dom (Pag .append Pbg)
by A90, A99, FINSEQ_3:27;
then consider n1 being
Element of
NAT such that A107:
n1 < len Pbg
and A108:
n = (len Pag) + n1
by A106, GLIB_001:35;
A109:
(Pag .append Pbg) . ((len Pag) + n1) = Pbg . (n1 + 1)
by A83, A52, A57, A49, A107, GLIB_001:34;
reconsider n1 =
n1 as
even Element of
NAT by A108;
reconsider n11 =
n1 + 1 as
odd Element of
NAT ;
A110:
n11 <= len Pbg
by A107, NAT_1:13;
then A111:
Pbg . n11 in the_Vertices_of Gb1
by GLIB_001:8;
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, A104, A111, XBOOLE_0:def 3;
suppose A112:
(
Pag . m in A &
Pbg . n11 in {xg,yg} )
;
contradictionper cases
( Pbg . n11 = Pag . 1 or Pbg . n11 = Pag . (len Pag) )
by A64, A52, A112, TARSKI:def 2;
suppose A113:
Pbg . n11 = Pag . 1
;
contradictionnow assume A114:
1
+ 2
>= m
;
contradictionper cases
( 1 + 2 > m or 1 + 2 = m )
by A114, XXREAL_0:1;
suppose A115:
1
+ 2
= m
;
contradictionthen A116:
1
+ 1
< len Pag
by A103, XXREAL_0:2;
then
1
+ 1
in dom Pag
by FINSEQ_3:27;
then A117:
Pag . (1 + 1) = (Pag .append Pbg) . (1 + 1)
by GLIB_001:33;
1
< (len Pag) - 1
by A116, XREAL_1:22;
then
1
+ 0 < ((len Pag) - 1) + (len Pbg)
by XREAL_1:10;
then A118:
(Pag .append Pbg) . (1 + 1) in (Pag .append Pbg) .edges()
by A84, GLIB_001:101, JORDAN12:3;
1
< len Pag
by A100, A103, XXREAL_0:2;
then
Pag . (1 + 1) Joins Pag . 1,
Pag . m,
G
by A115, GLIB_001:def 3, JORDAN12:3;
hence
contradiction
by A93, A105, A108, A109, A113, A117, A118, GLIB_000:17;
verum end; end; then
Pag is
chordal
by A98, A96, A103, A105, A108, A109, A113, Th85, JORDAN12:3;
then
Pa is
chordal
by A36, Th87;
hence
contradiction
by A48, Th89;
verum suppose A119:
Pbg . n11 = Pag . (len Pag)
;
contradictionnow set L =
len Pag;
assume A120:
m + 2
>= len Pag
;
contradictionper cases
( m + 2 = len Pag or m + 2 > len Pag )
by A120, XXREAL_0:1;
suppose A121:
m + 2
= len Pag
;
contradictionthen A122:
len Pag = (m + 1) + 1
;
then A123:
m + 1
< len Pag
by NAT_1:13;
1
<= m + 1
by NAT_1:12;
then
m + 1
in dom Pag
by A123, FINSEQ_3:27;
then A124:
Pag . (m + 1) = (Pag .append Pbg) . (m + 1)
by GLIB_001:33;
m < (len Pag) - 1
by A122, NAT_1:13;
then
m + 0 < ((len Pag) - 1) + (len Pbg)
by XREAL_1:10;
then A125:
(Pag .append Pbg) . (m + 1) in (Pag .append Pbg) .edges()
by A84, GLIB_001:101;
m < len Pag
by A123, NAT_1:13;
then
Pag . (m + 1) Joins Pag . m,
Pag . (len Pag),
G
by A97, A121, GLIB_001:def 3;
hence
contradiction
by A93, A105, A108, A109, A119, A124, A125;
verum end; end; then
Pag is
chordal
by A98, A92, A105, A108, A109, A119, Th85;
then
Pa is
chordal
by A36, Th87;
hence
contradiction
by A48, Th89;
verum suppose A126:
(
Pag . m in A &
Pbg . n11 in B )
;
contradictionthen reconsider bc =
Pb . n11 as
Vertex of
Gb by GLIB_000:def 39;
reconsider ac =
Pa . m as
Vertex of
Ga by A126, GLIB_000:def 39;
set WAB =
Gns .walkOf ac,
e,
bc;
e Joins ac,
bc,
Gns
by A16, A24, A95, A105, A108, A109, A126, Th19;
then A127:
Gns .walkOf ac,
e,
bc is_Walk_from ac,
bc
by GLIB_001:16;
b in B
by GLIB_002:9;
then reconsider bb =
b as
Vertex of
Gb 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;
consider WA being
Walk of
Ga such that A128:
WA is_Walk_from aa,
ac
by GLIB_002:def 1;
consider WB being
Walk of
Gb such that A129:
WB is_Walk_from bc,
bb
by GLIB_002:def 1;
reconsider WA =
WA,
WB =
WB as
Walk of
Gns by GLIB_001:168;
reconsider WAs =
WA,
WBs =
WB as
Walk of
Gns ;
A130:
WBs is_Walk_from bc,
bb
by A129, GLIB_001:20;
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 A128, GLIB_001:20;
then
WAs .append (Gns .walkOf ac,e,bc) is_Walk_from aa,
bc
by A127, GLIB_001:32;
then
(WAs .append (Gns .walkOf ac,e,bc)) .append WBs is_Walk_from a,
b
by A130, GLIB_001:32;
hence
contradiction
by A1, A2, Def8;
verum end; suppose
(
Pag . m in {xg,yg} &
Pbg . n11 in B )
;
contradictionthen
(
Pag . m = x or
Pag . m = y )
by TARSKI:def 2;
then A131:
Pag . m =
x
by A64, A52, A97, A103, GLIB_001:def 28
.=
Pbg . (len Pbg)
by A43, A45, A53, GLIB_001:def 23
;
now set L =
len Pbg;
assume A132:
n11 + 2
>= len Pbg
;
contradictionper cases
( n11 + 2 = len Pbg or n11 + 2 > len Pbg )
by A132, XXREAL_0:1;
suppose A133:
n11 + 2
= len Pbg
;
contradictionthen A134:
len Pbg = (n11 + 1) + 1
;
then
n11 < (len Pbg) - 1
by NAT_1:13;
then A135:
(len Pag) + n11 < ((len Pbg) - 1) + (len Pag)
by XREAL_1:8;
n11 + 1
< len Pbg
by A134, NAT_1:13;
then A136:
n11 < len Pbg
by NAT_1:13;
then
Pbg . (n11 + 1) Joins Pbg . n11,
Pbg . (len Pbg),
Gb1
by A133, GLIB_001:def 3;
then
Pbg . (n11 + 1) Joins Pbg . (len Pbg),
Pbg . n11,
Gb1
by GLIB_000:17;
then A137:
Pbg . (n11 + 1) Joins Pbg . (len Pbg),
Pbg . n11,
G
by GLIB_000:75;
A138:
1
<= (len Pag) + n11
by HEYTING3:1, NAT_1:12;
Pbg . (n11 + 1) = (Pag .append Pbg) . ((len Pag) + n11)
by A83, A52, A57, A49, A136, GLIB_001:34;
then
Pbg . (n11 + 1) in (Pag .append Pbg) .edges()
by A84, A138, A135, GLIB_001:100;
hence
contradiction
by A93, A105, A108, A109, A131, A137;
verum end; end; then
Pbg is
chordal
by A61, A96, A105, A108, A109, A131, Th85;
then
Pb is
chordal
by A31, Th87;
hence
contradiction
by A46, Th89;
verum end; suppose A139:
(
Pag . m in {xg,yg} &
Pbg . n11 in {xg,yg} )
;
contradictionthen A140:
(
Pbg . n11 = x or
Pbg . n11 = y )
by TARSKI:def 2;
(
Pag . m = x or
Pag . m = y )
by A139, TARSKI:def 2;
then
xg,
yg are_adjacent
by A91, A92, A105, A108, A109, A140, Def3;
hence
contradiction
by A4, A11, Th45;
verum end; end; suppose A141:
len Pag <= m
;
contradictionthen consider m1 being
Nat such that A142:
m = (len Pag) + m1
by NAT_1:10;
n > len Pag
by A94, A141, XXREAL_0:2;
then A143:
not
n in dom Pag
by FINSEQ_3:27;
n in dom (Pag .append Pbg)
by A90, A99, FINSEQ_3:27;
then consider n1 being
Element of
NAT such that A144:
n1 < len Pbg
and A145:
n = (len Pag) + n1
by A143, GLIB_001:35;
A146:
(Pag .append Pbg) . ((len Pag) + n1) = Pbg . (n1 + 1)
by A83, A52, A57, A49, A144, GLIB_001:34;
A147:
m1 in NAT
by ORDINAL1:def 13;
A148:
m1 < n1
by A94, A142, A145, XREAL_1:8;
then
m1 < len Pbg
by A144, XXREAL_0:2;
then A149:
(Pag .append Pbg) . ((len Pag) + m1) = Pbg . (m1 + 1)
by A83, A52, A57, A49, A147, GLIB_001:34;
reconsider n1 =
n1,
m1 =
m1 as
even Element of
NAT by A142, A145, ORDINAL1:def 13;
reconsider m11 =
m1 + 1,
n11 =
n1 + 1 as
odd Element of
NAT ;
A150:
m11 < n11
by A148, XREAL_1:8;
n11 <= len Pbg
by A144, NAT_1:13;
then A151:
m11 < len Pbg
by A150, XXREAL_0:2;
A152:
now assume A153:
m11 + 2
>= n11
;
contradictionper cases
( m11 + 2 = n11 or m11 + 2 > n11 )
by A153, XXREAL_0:1;
suppose A154:
m11 + 2
= n11
;
contradictionthen
m11 + 1
< len Pbg
by A144;
then
m11 < (len Pbg) - 1
by XREAL_1:22;
then A155:
(len Pag) + m11 < ((len Pbg) - 1) + (len Pag)
by XREAL_1:8;
A156:
1
<= (len Pag) + m11
by HEYTING3:1, NAT_1:12;
A157:
Pbg . (m11 + 1) Joins Pbg . m11,
Pbg . n11,
G
by A151, A154, GLIB_001:def 3;
Pbg . (m11 + 1) = (Pag .append Pbg) . ((len Pag) + m11)
by A83, A52, A57, A49, A151, GLIB_001:34;
then
Pbg . (m11 + 1) in (Pag .append Pbg) .edges()
by A84, A156, A155, GLIB_001:100;
hence
contradiction
by A93, A142, A145, A146, A149, A157;
verum end; end;
n11 <= len Pbg
by A144, NAT_1:13;
then
Pbg is
chordal
by A61, A92, A142, A145, A146, A149, A152, Th85;
then
Pb is
chordal
by A31, Th87;
hence
contradiction
by A46, Th89;
verum end;