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:
assume A2: for Gk being finite _Graph st Gk .order() < k holds
S₁[Gk] ; :: thesis:
let Gk1 be finite _Graph; :: thesis:
assume that
A3: Gk1 .order() = k and
A4: not Gk1 is trivial and
A5: Gk1 is chordal and
A6: not Gk1 is complete ; :: thesis:
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, Def6;
consider S being VertexSeparator of a,b such that
A9: S is minimal by Th79;
consider Gns being removeVertices of G,S;
reconsider sa = a, sb = b as Vertex of Gns by A7, A8, Th77;
set A = Gns .reachableFrom sa;
set B = Gns .reachableFrom sb;
consider Gas being inducedSubgraph of G,((Gns .reachableFrom sa) \/ S);
A10: Gns .reachableFrom sa c= the_Vertices_of Gns ;
then A11: Gns .reachableFrom sa c= the_Vertices_of G by XBOOLE_1:1;
then A12: (Gns .reachableFrom sa) \/ S is non empty Subset of (the_Vertices_of G) by XBOOLE_1:8;
A13: (Gns .reachableFrom sa) /\ (Gns .reachableFrom sb) = {} by A7, A8, Th76;

A14: now

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

end;

A17: now

assume Gas .order() = k ; :: thesis:
then A18: the_Vertices_of Gas = the_Vertices_of G by A3, PRE_POLY:8;
the_Vertices_of Gas = (Gns .reachableFrom sa) \/ S by A12, GLIB_000:def 39;
hence contradiction by A14, A18; :: thesis:

end;

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

A21: now

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

end;

A24: now

assume Gbs .order() = k ; :: thesis:
then A25: the_Vertices_of Gbs = the_Vertices_of G by A3, PRE_POLY:8;
the_Vertices_of Gbs = (Gns .reachableFrom sb) \/ S by A20, GLIB_000:def 39;
hence contradiction by A21, A25; :: thesis:

end;

consider Gs being 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 Gns = (the_Vertices_of G) \ S by GLIB_000:def 39;
Gbs .order() <= k by A3, GLIB_000:78;
then A27: Gbs .order() < k by A24, XXREAL_0:1;
ex b being Vertex of Gk1 st
( b in Gns .reachableFrom sb & b is simplicial )

proof

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

proof

per cases ;

suppose Gbs is complete ; :: thesis:

then a is simplicial by Th64;
hence ex c being Vertex of Gbs st
( c in Gns .reachableFrom sb & c is simplicial ) by A28; :: thesis:

end;

suppose A30: not Gbs is complete ; :: thesis:

then not Gbs is trivial ;
then consider a2, b2 being Vertex of Gbs 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

assume that
A35: a2 in S and
A36: b2 in S ; :: thesis:
reconsider a4 = a2, b4 = b2 as Vertex of Gs by A35, A36, GLIB_000:def 39;
Gs is complete by A7, A8, A9, A35, Th98;
then A37: a4,b4 are_adjacent by A31, Def6;
reconsider a3 = a2, b3 = b2 as Vertex of G by A35, A36;
not a3,b3 are_adjacent by A20, A32, Th45;
hence contradiction by A35, A37, Th45; :: thesis:

end;

then ( b2 in Gns .reachableFrom sb or a2 in Gns .reachableFrom sb ) by A29, XBOOLE_0:def 3;
hence ex c being Vertex of Gbs st
( c in Gns .reachableFrom sb & c is simplicial ) by A33, A34; :: thesis:

end;

then consider cc being Vertex of Gbs such that
A38: cc in Gns .reachableFrom sb and
A39: cc is simplicial ;
reconsider c = cc as Vertex of Gk1 by A19, A38;

now

let x be set ; :: thesis:
assume A40: x in Gk1 .AdjacentSet {c} ; :: thesis:
assume A41: not x in (Gns .reachableFrom sb) \/ S ; :: thesis:
then A42: not x in Gns .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, Th52;
then consider e being set such that
A44: e Joins c,x,Gk1 by Def3;
x in the_Vertices_of Gns by A26, A43, XBOOLE_0:def 5;
then e Joins c,x,Gns by A26, A38, A44, Th19;
hence contradiction by A38, A42, GLIB_002:10; :: thesis:

end;

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

end;

then consider b being Vertex of Gk1 such that
A46: b in Gns .reachableFrom sb and
A47: b is simplicial ;
Gas .order() <= k by A3, GLIB_000:78;
then A48: Gas .order() < k by A17, XXREAL_0:1;
ex a being Vertex of Gk1 st
( a in Gns .reachableFrom sa & a is simplicial )

proof

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

proof

per cases ;

suppose Gas is complete ; :: thesis:

then a is simplicial by Th64;
hence ex c being Vertex of Gas st
( c in Gns .reachableFrom sa & c is simplicial ) by A49; :: thesis:

end;

suppose A51: not Gas is complete ; :: thesis:

then not Gas is trivial ;
then consider a2, b2 being Vertex of Gas 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

assume that
A56: a2 in S and
A57: b2 in S ; :: thesis:
reconsider a4 = a2, b4 = b2 as Vertex of Gs by A56, A57, GLIB_000:def 39;
Gs is complete by A7, A8, A9, A56, Th98;
then A58: a4,b4 are_adjacent by A52, Def6;
reconsider a3 = a2, b3 = b2 as Vertex of G by A56, A57;
not a3,b3 are_adjacent by A12, A53, Th45;
hence contradiction by A56, A58, Th45; :: thesis:

end;

then ( b2 in Gns .reachableFrom sa or a2 in Gns .reachableFrom sa ) by A50, XBOOLE_0:def 3;
hence ex c being Vertex of Gas st
( c in Gns .reachableFrom sa & c is simplicial ) by A54, A55; :: thesis:

end;

then consider cc being Vertex of Gas such that
A59: cc in Gns .reachableFrom sa and
A60: cc is simplicial ;
reconsider c = cc as Vertex of Gk1 by A11, A59;

now

let x be set ; :: thesis:
assume A61: x in Gk1 .AdjacentSet {c} ; :: thesis:
assume A62: not x in (Gns .reachableFrom sa) \/ S ; :: thesis:
then A63: not x in Gns .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, Th52;
then consider e being set such that
A65: e Joins c,x,Gk1 by Def3;
x in the_Vertices_of Gns by A26, A64, XBOOLE_0:def 5;
then e Joins c,x,Gns by A26, A59, A65, Th19;
hence contradiction by A59, A63, GLIB_002:10; :: thesis:

end;

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

end;

then consider a being Vertex of Gk1 such that
A67: a in Gns .reachableFrom sa and
A68: a is simplicial ;

A69: now

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

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:

end;

A71: for G being finite _Graph holds S₁[G] from CHORD:sch 1(A1);
let G be finite non trivial chordal _Graph; :: thesis:
assume not G is complete ; :: thesis:
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: