defpred S_{1}[ finite _Graph] means ( G is chordal implies ex S being VertexScheme of G st S is perfect );

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

A1: now :: thesis: 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]

for G being finite _Graph holds SS

for Gk1 being finite _Graph st Gk1 .order() = k 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 A3: Gk1 .order() = k ; :: thesis: S_{1}[Gk1]

thus S_{1}[Gk1]
:: 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 A3: Gk1 .order() = k ; :: thesis: S

thus S

proof

assume A4:
Gk1 is chordal
; :: thesis: ex S being VertexScheme of Gk1 st S is perfect

end;per cases
( k = 1 or k <> 1 )
;

end;

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

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

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

end;

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

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

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