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
let P be Walk of G; :: according to CHORD:def 11 :: thesis: ( P .length() > 3 & P is Cycle-like implies P is chordal )
assume A2:
( P .length() > 3 & P is Cycle-like )
; :: thesis: P is chordal
A3:
P is Path-like
by A2;
A4:
not P .vertices() is empty
by GLIB_001:89;
rng S = the_Vertices_of G
by Def12;
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 A4, Th15;
reconsider x = x as Vertex of G by A5;
set n = x .. S;
A7:
rng S = the_Vertices_of G
by Def12;
then A8:
x .. S <= len S
by FINSEQ_4:31;
A9:
x .. S in dom S
by A7, FINSEQ_4:30;
A10:
S is one-to-one
by Def12;
then A12:
P .vertices() c= S .followSet (x .. S)
by TARSKI:def 3;
consider H being inducedSubgraph of G,(S .followSet (x .. S));
A13:
rng S = the_Vertices_of G
by Def12;
then A14:
x .. S <= len S
by FINSEQ_4:31;
x in S .followSet (x .. S)
by A7, A9, A10, Th16;
then reconsider y = x as Vertex of H by GLIB_000:def 39;
S . (x .. S) = x
by A13, FINSEQ_4:29;
then A15:
y is simplicial
by A1, A14, Def13;
A16:
not S .followSet (x .. S) is empty
by A8, Th107;
then reconsider C = P as Walk of H by A12, Th23;
reconsider C = C as Path of H by A3, GLIB_001:177;
( not P is trivial & P is closed )
by A2;
then
( not C is trivial & C is closed )
by GLIB_001:177;
then A17:
C is Cycle-like
by GLIB_001:def 31;
A18:
C .length() > 3
by A2, GLIB_001:115;
y in C .vertices()
by A5, GLIB_001:99;
then consider a, b being odd Nat such that
A19:
( a + 2 < b & b <= len C )
and
A20:
( C . a <> C . b & C . a in H .AdjacentSet {y} & C . b in H .AdjacentSet {y} )
and
A21:
for e being set st e in C .edges() holds
not e Joins C . a,C . b,H
by A17, A18, Th55;
consider e being set such that
A22:
e Joins C . a,C . b,H
by A15, A20, Th68;
C is chordal
by A19, A20, A21, A22, Def10;
hence
P is chordal
by A16, Th87; :: thesis: verum