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;

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;

not C is trivial by A4, GLIB_001:176;

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

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)

then
P .vertices() c= S .followSet (x .. S)
;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;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

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;

not C is trivial by A4, GLIB_001:176;

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