let G be finite chordal _Graph; :: thesis: (((LexBFS:CSeq G) .Result() ) `1 ) " is perfect VertexScheme of G
set Hh = ((LexBFS:CSeq G) .Result() ) `1 ;
A2: ((LexBFS:CSeq G) .Result() ) `1 is with_property_L3 by Th65;
A3: dom (((LexBFS:CSeq G) .Result() ) `1 ) = the_Vertices_of G by Th61;
reconsider V = (((LexBFS:CSeq G) .Result() ) `1 ) " as VertexScheme of G by Th62;
((LexBFS:CSeq G) .Result() ) `1 = ((LexBFS:CSeq G) ``1 ) .Result() by VNS1;
then ((LexBFS:CSeq G) .Result() ) `1 is one-to-one by Th25;
then V " = ((LexBFS:CSeq G) .Result() ) `1 by FUNCT_1:65;
hence (((LexBFS:CSeq G) .Result() ) `1 ) " is perfect VertexScheme of G by A2, A3, Th66; :: thesis: verum