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

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