let G, H be finite chordal _Graph; :: thesis: for g being perfect VertexScheme of G st G == H holds

g is perfect VertexScheme of H

let g be perfect VertexScheme of G; :: thesis: ( G == H implies g is perfect VertexScheme of H )

assume A1: G == H ; :: thesis: g is perfect VertexScheme of H

reconsider h = g as VertexScheme of H by A1, Th105;

g is perfect VertexScheme of H

let g be perfect VertexScheme of G; :: thesis: ( G == H implies g is perfect VertexScheme of H )

assume A1: G == H ; :: thesis: g is perfect VertexScheme of H

reconsider h = g as VertexScheme of H by A1, Th105;

now :: thesis: for n being non zero Nat st n <= len h holds

for Hf being inducedSubgraph of H,(h .followSet n)

for vh being Vertex of Hf st vh = h . n holds

vh is simplicial

hence
g is perfect VertexScheme of H
by Def13; :: thesis: verumfor Hf being inducedSubgraph of H,(h .followSet n)

for vh being Vertex of Hf st vh = h . n holds

vh is simplicial

let n be non zero Nat; :: thesis: ( n <= len h implies for Hf being inducedSubgraph of H,(h .followSet n)

for vh being Vertex of Hf st vh = h . n holds

vh is simplicial )

assume A2: n <= len h ; :: thesis: for Hf being inducedSubgraph of H,(h .followSet n)

for vh being Vertex of Hf st vh = h . n holds

vh is simplicial

let Hf be inducedSubgraph of H,(h .followSet n); :: thesis: for vh being Vertex of Hf st vh = h . n holds

vh is simplicial

let vh be Vertex of Hf; :: thesis: ( vh = h . n implies vh is simplicial )

assume A3: vh = h . n ; :: thesis: vh is simplicial

G .edgesBetween (g .followSet n) = H .edgesBetween (g .followSet n) by A1, GLIB_000:90;

then reconsider Gf = Hf as inducedSubgraph of G,(g .followSet n) by A1, GLIB_000:95;

reconsider vg = vh as Vertex of Gf ;

vg is simplicial by A2, A3, Def13;

hence vh is simplicial ; :: thesis: verum

end;for vh being Vertex of Hf st vh = h . n holds

vh is simplicial )

assume A2: n <= len h ; :: thesis: for Hf being inducedSubgraph of H,(h .followSet n)

for vh being Vertex of Hf st vh = h . n holds

vh is simplicial

let Hf be inducedSubgraph of H,(h .followSet n); :: thesis: for vh being Vertex of Hf st vh = h . n holds

vh is simplicial

let vh be Vertex of Hf; :: thesis: ( vh = h . n implies vh is simplicial )

assume A3: vh = h . n ; :: thesis: vh is simplicial

G .edgesBetween (g .followSet n) = H .edgesBetween (g .followSet n) by A1, GLIB_000:90;

then reconsider Gf = Hf as inducedSubgraph of G,(g .followSet n) by A1, GLIB_000:95;

reconsider vg = vh as Vertex of Gf ;

vg is simplicial by A2, A3, Def13;

hence vh is simplicial ; :: thesis: verum