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 ;
now :: thesis: for n being non zero Nat st n <= len h holds
for Hf being inducedSubgraph of H,()
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,()
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,()
for vh being Vertex of Hf st vh = h . n holds
vh is simplicial

let Hf be inducedSubgraph of H,(); :: 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 () = H .edgesBetween () by ;
then reconsider Gf = Hf as inducedSubgraph of G,() by ;
reconsider vg = vh as Vertex of Gf ;
vg is simplicial by ;
hence vh is simplicial ; :: thesis: verum
end;
hence g is perfect VertexScheme of H by Def13; :: thesis: verum