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 ;
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 ;
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 ;
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 ;
reconsider C = C as Path of the inducedSubgraph of G,(S .followSet (x .. S)) by ;
A12: C is closed by ;
A13: y in C .vertices() by ;
A14: rng S = the_Vertices_of G by Def12;
then A15: S . (x .. S) = x by FINSEQ_4:19;
not C is trivial by ;
then A16: C is Cycle-like by A12;
C .length() > 3 by ;
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 ;
x .. S <= len S by ;
then y is simplicial by ;
then ex e being object st e Joins C . a,C . b, the inducedSubgraph of G,(S .followSet (x .. S)) by ;
then C is chordal by A17, A18, A19, A22;
hence P is chordal by ; :: thesis: verum