defpred S_{1}[ 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_{1}[Gk] ) holds

for Gk1 being finite _Graph st Gk1 .order() = k holds

S_{1}[Gk1]
_{1}[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

( 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

for Gk1 being finite _Graph st Gk1 .order() = k holds

S

proof

A71:
for G being finite _Graph holds S
let k be non zero Nat; :: thesis: ( ( for Gk being finite _Graph st Gk .order() < k holds

S_{1}[Gk] ) implies for Gk1 being finite _Graph st Gk1 .order() = k holds

S_{1}[Gk1] )

assume A2: for Gk being finite _Graph st Gk .order() < k holds

S_{1}[Gk]
; :: thesis: for Gk1 being finite _Graph st Gk1 .order() = k holds

S_{1}[Gk1]

let Gk1 be finite _Graph; :: thesis: ( Gk1 .order() = k implies S_{1}[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;

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;

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 )

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 )

A67: a in the removeVertices of G,S .reachableFrom sa and

A68: a is simplicial ;

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;S

S

assume A2: for Gk being finite _Graph st Gk .order() < k holds

S

S

let Gk1 be finite _Graph; :: thesis: ( Gk1 .order() = k implies S

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;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

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

set Gbs = the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S);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;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

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;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

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

set Gs = the inducedSubgraph of G,S;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;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

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

then consider b being Vertex of Gk1 such that
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 )

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;

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;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
end;

then consider cc being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sb) \/ S) such that 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 )
;

end;

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 )

( 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;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

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 )

( 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;

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;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 )

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;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;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

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

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

then A45:
Gk1 .AdjacentSet {c} c= ( the removeVertices of G,S .reachableFrom sb) \/ S
;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;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

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

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

then consider a being Vertex of Gk1 such that
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 )

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;

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;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
end;

then consider cc being Vertex of the inducedSubgraph of G,(( the removeVertices of G,S .reachableFrom sa) \/ S) such that 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 )
;

end;

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 )

( 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;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

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 )

( 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;

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;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 )

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;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;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

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

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

then A66:
Gk1 .AdjacentSet {c} c= ( the removeVertices of G,S .reachableFrom sa) \/ S
;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;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

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

A67: a in the removeVertices of G,S .reachableFrom sa and

A68: a is simplicial ;

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

a <> b
by A13, A67, A46, XBOOLE_0:def 4;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;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

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

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