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:43;
((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