defpred S1[ 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
S1[Gk] ) holds
for Gk1 being finite _Graph st Gk1 .order() = k holds
S1[Gk1]
proof
let k be non zero Nat; :: thesis: ( ( for Gk being finite _Graph st Gk .order() < k holds
S1[Gk] ) implies for Gk1 being finite _Graph st Gk1 .order() = k holds
S1[Gk1] )

assume A2: for Gk being finite _Graph st Gk .order() < k holds
S1[Gk] ; :: thesis: for Gk1 being finite _Graph st Gk1 .order() = k holds
S1[Gk1]

let Gk1 be finite _Graph; :: thesis: ( Gk1 .order() = k implies S1[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 () 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) \/ Send;
A17: now :: thesis: not the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) .order() = kend;
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 ;
then A20: ( the removeVertices of G,S .reachableFrom sb) \/ S is non empty Subset of () by XBOOLE_1:8;
A21: now :: thesis: not a in ( the removeVertices of G,S .reachableFrom sb) \/ Send;
A24: now :: thesis: not the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) .order() = kend;
set Gs = the inducedSubgraph of G,S;
not a in S by A7, A8, Def8;
then a in () \ S by XBOOLE_0:def 5;
then A26: the_Vertices_of the removeVertices of G,S = () \ S by GLIB_000:def 37;
the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) .order() <= k by ;
then A27: the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) .order() < k by ;
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 ;
then reconsider a = aa as Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) by ;
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 )

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
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 ;
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 ;
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 ;
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 ; :: 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 ;
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 ;
reconsider x = x as Vertex of Gk1 by A40;
then consider e being object such that
A44: e Joins c,x,Gk1 ;
x in the_Vertices_of the removeVertices of G,S by ;
then e Joins c,x, the removeVertices of G,S by ;
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 ;
then c is simplicial by ;
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 ;
then A48: the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) .order() < k by ;
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 ;
then reconsider a = aa as Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) by ;
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 )

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
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 ;
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 ;
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 ;
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 ; :: 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 ;
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 ;
reconsider x = x as Vertex of Gk1 by A61;
then consider e being object such that
A65: e Joins c,x,Gk1 ;
x in the_Vertices_of the removeVertices of G,S by ;
then e Joins c,x, the removeVertices of G,S by ;
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 ;
then c is simplicial by ;
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 ;
then consider e being object such that
A70: e Joins a,b,Gk1 ;
e Joins aa,bb, the removeVertices of G,S by ;
then bb in the removeVertices of G,S .reachableFrom sa by ;
hence contradiction by A13, A46, XBOOLE_0:def 4; :: thesis: verum
end;
a <> b by ;
hence ex a, b being Vertex of Gk1 st
( a <> b & not a,b are_adjacent & a is simplicial & b is simplicial ) by ; :: thesis: verum
end;
A71: for G being finite _Graph holds S1[G] from 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