defpred S₁[ _finite _Graph] means ( not $1 is _trivial & $1 is chordal & not $1 is complete implies ex a, b being Vertex of $1 st
( a <> b & not a,b are_adjacent & a is simplicial & b is simplicial ) );
A1: for k being non zero Nat st ( for Gk being _finite _Graph st Gk .order() < k holds
S₁[Gk] ) holds
for Gk1 being _finite _Graph st Gk1 .order() = k holds
S₁[Gk1]

proof

let k be non zero Nat; :: thesis: ( ( for Gk being _finite _Graph st Gk .order() < k holds
S₁[Gk] ) implies for Gk1 being _finite _Graph st Gk1 .order() = k holds
S₁[Gk1] )
assume A2: for Gk being _finite _Graph st Gk .order() < k holds
S₁[Gk] ; :: thesis: for Gk1 being _finite _Graph st Gk1 .order() = k holds
S₁[Gk1]
let Gk1 be _finite _Graph; :: thesis: ( Gk1 .order() = k implies S₁[Gk1] )
assume that
A3: Gk1 .order() = k and
A4: not Gk1 is _trivial and
A5: Gk1 is chordal and
A6: not Gk1 is complete ; :: thesis: ex a, b being Vertex of Gk1 st
( a <> b & not a,b are_adjacent & a is simplicial & b is simplicial )
reconsider G = Gk1 as _finite non _trivial chordal _Graph by A4, A5;
consider a, b being Vertex of G such that
A7: a <> b and
A8: not a,b are_adjacent by A6;
consider S being VertexSeparator of a,b such that
A9: S is minimal by Th78;
set Gns = the removeVertices of G,S;
reconsider sa = a, sb = b as Vertex of the removeVertices of G,S by A7, A8, Th76;
set A = the removeVertices of G,S .reachableFrom sa;
set B = the removeVertices of G,S .reachableFrom sb;
set Gas = the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S);
A10: the removeVertices of G,S .reachableFrom sa c= the_Vertices_of the removeVertices of G,S ;
then A11: the removeVertices of G,S .reachableFrom sa c= the_Vertices_of G by XBOOLE_1:1;
then A12: ( the removeVertices of G,S .reachableFrom sa) \/ S is non empty Subset of (the_Vertices_of G) by XBOOLE_1:8;
A13: ( the removeVertices of G,S .reachableFrom sa) /\ ( the removeVertices of G,S .reachableFrom sb) = {} by A7, A8, Th75;

A14: now :: thesis: not b in ( the removeVertices of G,S .reachableFrom sa) \/ S

assume A15: b in ( the removeVertices of G,S .reachableFrom sa) \/ S ; :: thesis: contradiction
not b in S by A7, A8, Def8;
then A16: b in the removeVertices of G,S .reachableFrom sa by A15, XBOOLE_0:def 3;
b in the removeVertices of G,S .reachableFrom sb by GLIB_002:9;
hence contradiction by A13, A16, XBOOLE_0:def 4; :: thesis: verum

end;

A17: now :: thesis: not the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) .order() = k

assume the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) .order() = k ; :: thesis: contradiction
then A18: the_Vertices_of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) = the_Vertices_of G by A3, CARD_2:102;
the_Vertices_of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) = ( the removeVertices of G,S .reachableFrom sa) \/ S by A12, GLIB_000:def 37;
hence contradiction by A14, A18; :: thesis: verum

end;

set Gbs = the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S);
A19: the removeVertices of G,S .reachableFrom sb c= the_Vertices_of G by A10, XBOOLE_1:1;
then A20: ( the removeVertices of G,S .reachableFrom sb) \/ S is non empty Subset of (the_Vertices_of G) by XBOOLE_1:8;

A21: now :: thesis: not a in ( the removeVertices of G,S .reachableFrom sb) \/ S

assume A22: a in ( the removeVertices of G,S .reachableFrom sb) \/ S ; :: thesis: contradiction
not a in S by A7, A8, Def8;
then A23: a in the removeVertices of G,S .reachableFrom sb by A22, XBOOLE_0:def 3;
a in the removeVertices of G,S .reachableFrom sa by GLIB_002:9;
hence contradiction by A13, A23, XBOOLE_0:def 4; :: thesis: verum

end;

A24: now :: thesis: not the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) .order() = k

assume the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) .order() = k ; :: thesis: contradiction
then A25: the_Vertices_of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) = the_Vertices_of G by A3, CARD_2:102;
the_Vertices_of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) = ( the removeVertices of G,S .reachableFrom sb) \/ S by A20, GLIB_000:def 37;
hence contradiction by A21, A25; :: thesis: verum

end;

set Gs = the inducedSubgraph of G,S;
not a in S by A7, A8, Def8;
then a in (the_Vertices_of G) \ S by XBOOLE_0:def 5;
then A26: the_Vertices_of the removeVertices of G,S = (the_Vertices_of G) \ S by GLIB_000:def 37;
the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) .order() <= k by A3, GLIB_000:75;
then A27: the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) .order() < k by A24, XXREAL_0:1;
ex b being Vertex of Gk1 st
( b in the removeVertices of G,S .reachableFrom sb & b is simplicial )

proof

consider aa being object such that
A28: aa in the removeVertices of G,S .reachableFrom sb by XBOOLE_0:def 1;
A29: the_Vertices_of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) = ( the removeVertices of G,S .reachableFrom sb) \/ S by A20, GLIB_000:def 37;
then reconsider a = aa as Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) by A28, XBOOLE_0:def 3;
ex c being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) st
( c in the removeVertices of G,S .reachableFrom sb & c is simplicial )

proof

per cases ( the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) is complete or not the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) is complete ) ;

suppose the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) is complete ; :: thesis: ex c being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) st
( c in the removeVertices of G,S .reachableFrom sb & c is simplicial )

then a is simplicial by Th63;
hence ex c being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) st
( c in the removeVertices of G,S .reachableFrom sb & c is simplicial ) by A28; :: thesis: verum

end;

suppose A30: not the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) is complete ; :: thesis: ex c being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) st
( c in the removeVertices of G,S .reachableFrom sb & c is simplicial )

then not the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) is _trivial ;
then consider a2, b2 being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) such that
A31: a2 <> b2 and
A32: not a2,b2 are_adjacent and
A33: a2 is simplicial and
A34: b2 is simplicial by A2, A27, A30;

now :: thesis: ( a2 in S implies not b2 in S )

assume that
A35: a2 in S and
A36: b2 in S ; :: thesis: contradiction
reconsider a4 = a2, b4 = b2 as Vertex of the inducedSubgraph of G,S by A35, A36, GLIB_000:def 37;
the inducedSubgraph of G,S is complete by A7, A8, A9, A35, Th97;
then A37: a4,b4 are_adjacent by A31;
reconsider a3 = a2, b3 = b2 as Vertex of G by A35, A36;
not a3,b3 are_adjacent by A20, A32, Th44;
hence contradiction by A35, A37, Th44; :: thesis: verum

end;

then ( b2 in the removeVertices of G,S .reachableFrom sb or a2 in the removeVertices of G,S .reachableFrom sb ) by A29, XBOOLE_0:def 3;
hence ex c being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) st
( c in the removeVertices of G,S .reachableFrom sb & c is simplicial ) by A33, A34; :: thesis: verum

end;

end;

end;

then consider cc being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) such that
A38: cc in the removeVertices of G,S .reachableFrom sb and
A39: cc is simplicial ;
reconsider c = cc as Vertex of Gk1 by A19, A38;

now :: thesis: for x being object st x in Gk1 .AdjacentSet {c} holds
x in ( the removeVertices of G,S .reachableFrom sb) \/ S

let x be object ; :: thesis: ( x in Gk1 .AdjacentSet {c} implies x in ( the removeVertices of G,S .reachableFrom sb) \/ S )
assume A40: x in Gk1 .AdjacentSet {c} ; :: thesis: x in ( the removeVertices of G,S .reachableFrom sb) \/ S
assume A41: not x in ( the removeVertices of G,S .reachableFrom sb) \/ S ; :: thesis: contradiction
then A42: not x in the removeVertices of G,S .reachableFrom sb by XBOOLE_0:def 3;
A43: not x in S by A41, XBOOLE_0:def 3;
reconsider x = x as Vertex of Gk1 by A40;
c,x are_adjacent by A40, Th51;
then consider e being object such that
A44: e Joins c,x,Gk1 ;
x in the_Vertices_of the removeVertices of G,S by A26, A43, XBOOLE_0:def 5;
then e Joins c,x, the removeVertices of G,S by A26, A38, A44, Th19;
hence contradiction by A38, A42, GLIB_002:10; :: thesis: verum

end;

then A45: Gk1 .AdjacentSet {c} c= ( the removeVertices of G,S .reachableFrom sb) \/ S ;
c in ( the removeVertices of G,S .reachableFrom sb) \/ S by A38, XBOOLE_0:def 3;
then c is simplicial by A20, A39, A45, Th66;
hence ex b being Vertex of Gk1 st
( b in the removeVertices of G,S .reachableFrom sb & b is simplicial ) by A38; :: thesis: verum

end;

then consider b being Vertex of Gk1 such that
A46: b in the removeVertices of G,S .reachableFrom sb and
A47: b is simplicial ;
the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) .order() <= k by A3, GLIB_000:75;
then A48: the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) .order() < k by A17, XXREAL_0:1;
ex a being Vertex of Gk1 st
( a in the removeVertices of G,S .reachableFrom sa & a is simplicial )

proof

consider aa being object such that
A49: aa in the removeVertices of G,S .reachableFrom sa by XBOOLE_0:def 1;
A50: the_Vertices_of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) = ( the removeVertices of G,S .reachableFrom sa) \/ S by A12, GLIB_000:def 37;
then reconsider a = aa as Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) by A49, XBOOLE_0:def 3;
ex c being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) st
( c in the removeVertices of G,S .reachableFrom sa & c is simplicial )

proof

per cases ( the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) is complete or not the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) is complete ) ;

suppose the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) is complete ; :: thesis: ex c being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) st
( c in the removeVertices of G,S .reachableFrom sa & c is simplicial )

then a is simplicial by Th63;
hence ex c being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) st
( c in the removeVertices of G,S .reachableFrom sa & c is simplicial ) by A49; :: thesis: verum

end;

suppose A51: not the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) is complete ; :: thesis: ex c being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) st
( c in the removeVertices of G,S .reachableFrom sa & c is simplicial )

then not the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) is _trivial ;
then consider a2, b2 being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) such that
A52: a2 <> b2 and
A53: not a2,b2 are_adjacent and
A54: a2 is simplicial and
A55: b2 is simplicial by A2, A48, A51;

now :: thesis: ( a2 in S implies not b2 in S )

assume that
A56: a2 in S and
A57: b2 in S ; :: thesis: contradiction
reconsider a4 = a2, b4 = b2 as Vertex of the inducedSubgraph of G,S by A56, A57, GLIB_000:def 37;
the inducedSubgraph of G,S is complete by A7, A8, A9, A56, Th97;
then A58: a4,b4 are_adjacent by A52;
reconsider a3 = a2, b3 = b2 as Vertex of G by A56, A57;
not a3,b3 are_adjacent by A12, A53, Th44;
hence contradiction by A56, A58, Th44; :: thesis: verum

end;

then ( b2 in the removeVertices of G,S .reachableFrom sa or a2 in the removeVertices of G,S .reachableFrom sa ) by A50, XBOOLE_0:def 3;
hence ex c being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) st
( c in the removeVertices of G,S .reachableFrom sa & c is simplicial ) by A54, A55; :: thesis: verum

end;

end;

end;

then consider cc being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) such that
A59: cc in the removeVertices of G,S .reachableFrom sa and
A60: cc is simplicial ;
reconsider c = cc as Vertex of Gk1 by A11, A59;

now :: thesis: for x being object st x in Gk1 .AdjacentSet {c} holds
x in ( the removeVertices of G,S .reachableFrom sa) \/ S

let x be object ; :: thesis: ( x in Gk1 .AdjacentSet {c} implies x in ( the removeVertices of G,S .reachableFrom sa) \/ S )
assume A61: x in Gk1 .AdjacentSet {c} ; :: thesis: x in ( the removeVertices of G,S .reachableFrom sa) \/ S
assume A62: not x in ( the removeVertices of G,S .reachableFrom sa) \/ S ; :: thesis: contradiction
then A63: not x in the removeVertices of G,S .reachableFrom sa by XBOOLE_0:def 3;
A64: not x in S by A62, XBOOLE_0:def 3;
reconsider x = x as Vertex of Gk1 by A61;
c,x are_adjacent by A61, Th51;
then consider e being object such that
A65: e Joins c,x,Gk1 ;
x in the_Vertices_of the removeVertices of G,S by A26, A64, XBOOLE_0:def 5;
then e Joins c,x, the removeVertices of G,S by A26, A59, A65, Th19;
hence contradiction by A59, A63, GLIB_002:10; :: thesis: verum

end;

then A66: Gk1 .AdjacentSet {c} c= ( the removeVertices of G,S .reachableFrom sa) \/ S ;
c in ( the removeVertices of G,S .reachableFrom sa) \/ S by A59, XBOOLE_0:def 3;
then c is simplicial by A12, A60, A66, Th66;
hence ex a being Vertex of Gk1 st
( a in the removeVertices of G,S .reachableFrom sa & a is simplicial ) by A59; :: thesis: verum

end;

then consider a being Vertex of Gk1 such that
A67: a in the removeVertices of G,S .reachableFrom sa and
A68: a is simplicial ;

A69: now :: thesis: not a,b are_adjacent

reconsider aa = a, bb = b as Vertex of the removeVertices of G,S by A67, A46;
assume a,b are_adjacent ; :: thesis: contradiction
then consider e being object such that
A70: e Joins a,b,Gk1 ;
e Joins aa,bb, the removeVertices of G,S by A26, A70, Th19;
then bb in the removeVertices of G,S .reachableFrom sa by A67, GLIB_002:10;
hence contradiction by A13, A46, XBOOLE_0:def 4; :: thesis: verum

end;

a <> b by A13, A67, A46, XBOOLE_0:def 4;
hence ex a, b being Vertex of Gk1 st
( a <> b & not a,b are_adjacent & a is simplicial & b is simplicial ) by A68, A47, A69; :: thesis: verum

end;

A71: for G being _finite _Graph holds S₁[G] from CHORD:sch 1(A1);
let G be _finite non _trivial chordal _Graph; :: thesis: ( not G is complete implies ex a, b being Vertex of G st
( a <> b & not a,b are_adjacent & a is simplicial & b is simplicial ) )
assume not G is complete ; :: thesis: ex a, b being Vertex of G st
( a <> b & not a,b are_adjacent & a is simplicial & b is simplicial )
hence ex a, b being Vertex of G st
( a <> b & not a,b are_adjacent & a is simplicial & b is simplicial ) by A71; :: thesis: verum