let G be finite chordal _Graph; :: thesis: (((LexBFS:CSeq G) .Result() ) `1 ) " is perfect VertexScheme of G
set Hh = ((LexBFS:CSeq G) .Result() ) `1 ;
reconsider V = (((LexBFS:CSeq G) .Result() ) `1 ) " as VertexScheme of G by Th50;
A1: dom (((LexBFS:CSeq G) .Result() ) `1 ) = the_Vertices_of G by Th49;
((LexBFS:CSeq G) .Result() ) `1 = ((LexBFS:CSeq G) ``1 ) .Result() by Th40;
then ((LexBFS:CSeq G) .Result() ) `1 is one-to-one by Th18;
then A2: V " = ((LexBFS:CSeq G) .Result() ) `1 by FUNCT_1:65;
((LexBFS:CSeq G) .Result() ) `1 is with_property_L3 by Th53;
hence (((LexBFS:CSeq G) .Result() ) `1 ) " is perfect VertexScheme of G by A1, A2, Th54; :: thesis: verum