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;

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

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;

hence g is perfect VertexScheme of H by Def13; :: thesis: verum