defpred S₁[ _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
S₁[Gk] ) holds
for Gk1 being _finite _Graph st Gk1 .order() = k holds
S₁[Gk1]

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 A3: Gk1 .order() = k ; :: thesis: S₁[Gk1]
thus S₁[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 A3, A4, GLIB_000:26;
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 = (the_Vertices_of G) \ {x} by GLIB_000:def 37;
the removeVertex of G,x .order() = card ((the_Vertices_of G) \ {x}) by A8, GLIB_000:def 37
.= (G .order()) - (card {x}) by CARD_2:44
.= k - 1 by A3, CARD_2:42 ;
then consider T being VertexScheme of the removeVertex of G,x such that
A10: T is perfect by A2, XREAL_1:146;
{x} /\ (rng T) = {x} /\ ((the_Vertices_of G) \ {x}) by A9, Def12
.= ({x} /\ (the_Vertices_of G)) \ {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 = (the_Vertices_of G) \ {x} by A9, Def12;
then rng (<*x*> ^ T) = ((the_Vertices_of G) \ {x}) \/ (rng <*x*>) by FINSEQ_1:31;
then rng (<*x*> ^ T) = ((the_Vertices_of G) \ {x}) \/ {x} by FINSEQ_1:38;
then rng (<*x*> ^ T) = {x} \/ (the_Vertices_of G) 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 A11, A7, FINSEQ_3:91;
then reconsider S = S as VertexScheme of Gk1 by A12, Def12;
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,(S .followSet n)
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,(S .followSet n)
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,(S .followSet n); :: 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 A14, XXREAL_0:1;

suppose A16: 1 = n ; :: thesis: v is simplicial

then A17: S .followSet n = rng S by FINSEQ_6:133
.= the_Vertices_of G by Def12 ;
x = v by A15, A16, FINSEQ_1:41;
hence v is simplicial by A6, A17, Th65, GLIB_000:94; :: thesis: verum

end;

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 A13, A18, FINSEQ_1:24;
A20: T .followSet n1 = S .followSet (n1 + 1) by Th17;
n + (- 1) <= (len S) + (- 1) by A13, XREAL_1:7;
then n1 <= ((len <*x*>) + (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 A9, A20, Th30;
hence v is simplicial by A10, A15, A19, A21; :: thesis: verum

end;

end;

end;

end;

end;

end;

for G being _finite _Graph holds S₁[G] from CHORD:sch 1(A1);
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