let G be _finite _Graph; :: thesis: ( ex S being VertexScheme of G st S is perfect implies G is chordal )
given S being VertexScheme of G such that A1: S is perfect ; :: thesis: G is chordal
A2: rng S = the_Vertices_of G by Def12;
let P be Walk of G; :: according to CHORD:def 11 :: thesis: ( P .length() > 3 & P is Cycle-like implies P is chordal )
assume that
A3: P .length() > 3 and
A4: P is Cycle-like ; :: thesis: P is chordal
not P .vertices() is empty by GLIB_001:88;
then consider x being set such that
A5: x in P .vertices() and
A6: for y being set st y in P .vertices() holds
x .. S <= y .. S by A2, Th15;
reconsider x = x as Vertex of G by A5;
set n = x .. S;
set H = the inducedSubgraph of G,(S .followSet (x .. S));
A7: rng S = the_Vertices_of G by Def12;
then A8: x .. S in dom S by FINSEQ_4:20;
A9: S is one-to-one by Def12;
then x in S .followSet (x .. S) by A7, A8, Th16;
then reconsider y = x as Vertex of the inducedSubgraph of G,(S .followSet (x .. S)) by GLIB_000:def 37;
A10: not S .followSet (x .. S) is empty by A7, Th106, FINSEQ_4:21;

now :: thesis: for y being object st y in P .vertices() holds
y in S .followSet (x .. S)

let y be object ; :: thesis: ( y in P .vertices() implies y in S .followSet (x .. S) )
assume A11: y in P .vertices() ; :: thesis: y in S .followSet (x .. S)
reconsider z = y as Vertex of G by A11;
x .. S <= z .. S by A6, A11;
hence y in S .followSet (x .. S) by A7, A8, A9, Th16; :: thesis: verum

end;

then P .vertices() c= S .followSet (x .. S) ;
then reconsider C = P as Walk of the inducedSubgraph of G,(S .followSet (x .. S)) by A10, Th23;
reconsider C = C as Path of the inducedSubgraph of G,(S .followSet (x .. S)) by A4, GLIB_001:176;
A12: C is closed by A4, GLIB_001:176;
A13: y in C .vertices() by A5, GLIB_001:98;
A14: rng S = the_Vertices_of G by Def12;
then A15: S . (x .. S) = x by FINSEQ_4:19;
C is trivial by A4;
then A16: C is Cycle-like by A12;
C .length() > 3 by A3, GLIB_001:114;
then consider a, b being odd Nat such that
A17: a + 2 < b and
A18: b <= len C and
A19: C . a <> C . b and
A20: C . a in the inducedSubgraph of G,(S .followSet (x .. S)) .AdjacentSet {y} and
A21: C . b in the inducedSubgraph of G,(S .followSet (x .. S)) .AdjacentSet {y} and
A22: for e being object st e in C .edges() holds
not e Joins C . a,C . b, the inducedSubgraph of G,(S .followSet (x .. S)) by A16, A13, Th54;
x .. S <= len S by A14, FINSEQ_4:21;
then y is simplicial by A1, A15;
then ex e being object st e Joins C . a,C . b, the inducedSubgraph of G,(S .followSet (x .. S)) by A19, A20, A21, Th67;
then C is chordal by A17, A18, A19, A22;
hence P is chordal by A10, Th86; :: thesis: verum