defpred S1[ finite _Graph] means ( G is chordal implies ex S being VertexScheme of G st S is perfect );
A1: now :: thesis: 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]
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 A3: Gk1 .order() = k ; :: thesis: S1[Gk1]
thus S1[Gk1] :: thesis: verum
proof
assume A4: Gk1 is chordal ; :: thesis: ex S being VertexScheme of Gk1 st S is perfect
per cases ( k = 1 or k <> 1 ) ;
suppose A5: k = 1 ; :: thesis: ex S being VertexScheme of Gk1 st S is perfect
set v = the Vertex of Gk1;
Gk1 is trivial by A3, A5;
then ex S being VertexScheme of Gk1 st
( S = <* the Vertex of Gk1*> & S is perfect ) by Th107;
hence ex S being VertexScheme of Gk1 st S is perfect ; :: thesis: verum
end;
suppose k <> 1 ; :: thesis: ex S being VertexScheme of Gk1 st S is perfect
then reconsider G = Gk1 as finite non trivial chordal _Graph by ;
consider x being Vertex of G such that
A6: x is simplicial by Th102;
set H = the removeVertex of G,x;
A7: <*x*> is one-to-one by FINSEQ_3:93;
A8: not (the_Vertices_of G) \ {x} is empty by GLIB_000:20;
then A9: the_Vertices_of the removeVertex of G,x = () \ {x} by GLIB_000:def 37;
the removeVertex of G,x .order() = card (() \ {x}) by
.= () - () by CARD_2:44
.= k - 1 by ;
then consider T being VertexScheme of the removeVertex of G,x such that
A10: T is perfect by ;
{x} /\ (rng T) = {x} /\ (() \ {x}) by
.= ({x} /\ ()) \ {x} by XBOOLE_1:49
.= {x} \ {x} by XBOOLE_1:28
.= {} by XBOOLE_1:37 ;
then {x} misses rng T ;
then A11: rng <*x*> misses rng T by FINSEQ_1:38;
set S = <*x*> ^ T;
rng T = () \ {x} by ;
then rng (<*x*> ^ T) = (() \ {x}) \/ () by FINSEQ_1:31;
then rng (<*x*> ^ T) = (() \ {x}) \/ {x} by FINSEQ_1:38;
then rng (<*x*> ^ T) = {x} \/ () by XBOOLE_1:39;
then A12: rng (<*x*> ^ T) = the_Vertices_of G by XBOOLE_1:12;
then reconsider S = <*x*> ^ T as FinSequence of the_Vertices_of G by FINSEQ_1:def 4;
T is one-to-one by Def12;
then S is one-to-one by ;
then reconsider S = S as VertexScheme of Gk1 by ;
take S ; :: thesis: S is perfect
let n be non zero Nat; :: according to CHORD:def 13 :: thesis: ( n <= len S implies for Gf being inducedSubgraph of Gk1,()
for v being Vertex of Gf st v = S . n holds
v is simplicial )

assume A13: n <= len S ; :: thesis: for Gf being inducedSubgraph of Gk1,()
for v being Vertex of Gf st v = S . n holds
v is simplicial

A14: 1 <= n by NAT_1:14;
let Gf be inducedSubgraph of Gk1,(); :: thesis: for v being Vertex of Gf st v = S . n holds
v is simplicial

let v be Vertex of Gf; :: thesis: ( v = S . n implies v is simplicial )
assume A15: v = S . n ; :: thesis: v is simplicial
per cases ( 1 = n or 1 < n ) by ;
suppose A18: 1 < n ; :: thesis: v is simplicial
then 1 + (- 1) < n + (- 1) by XREAL_1:8;
then reconsider n1 = n - 1 as non zero Element of NAT by INT_1:3;
len <*x*> = 1 by FINSEQ_1:39;
then A19: S . n = T . n1 by ;
A20: T .followSet n1 = S .followSet (n1 + 1) by Th17;
n + (- 1) <= (len S) + (- 1) by ;
then n1 <= (() + (len T)) + (- 1) by FINSEQ_1:22;
then A21: n1 <= (1 + (len T)) + (- 1) by FINSEQ_1:39;
then not T .followSet n1 is empty by Th106;
then Gf is inducedSubgraph of the removeVertex of G,x,(T .followSet n1) by ;
hence v is simplicial by A10, A15, A19, A21; :: thesis: verum
end;
end;
end;
end;
end;
end;
for G being finite _Graph holds S1[G] from then consider S being VertexScheme of G such that
A22: S is perfect ;
take S ; :: thesis: S is perfect
thus S is perfect by A22; :: thesis: verum