let G be finite _Graph; :: thesis: (((LexBFS:CSeq G) .Result() ) `1 ) " is VertexScheme of G
set CS = LexBFS:CSeq G;
set CSO = (LexBFS:CSeq G) . (G .order() );
set VLO = ((LexBFS:CSeq G) . (G .order() )) `1 ;
set VL = (LexBFS:CSeq G) ``1 ;
A1: (LexBFS:CSeq G) . (G .order() ) = (LexBFS:CSeq G) .Result() by Th37;
A2: (LexBFS:CSeq G) .Lifespan() = G .order() by Th37;
A3: ((LexBFS:CSeq G) . (G .order() )) `1 = ((LexBFS:CSeq G) ``1 ) . (G .order() ) by Def16;
then A4: ((LexBFS:CSeq G) . (G .order() )) `1 is one-to-one by Th18;
dom (((LexBFS:CSeq G) . (G .order() )) `1 ) = the_Vertices_of G by Th36;
then A5: rng ((((LexBFS:CSeq G) . (G .order() )) `1 ) " ) = the_Vertices_of G by A4, FUNCT_1:55;
(LexBFS:CSeq G) .Lifespan() = ((LexBFS:CSeq G) ``1 ) .Lifespan() by Th39;
then rng (((LexBFS:CSeq G) ``1 ) . (G .order() )) = (Seg (G .order() )) \ (Seg ((G .order() ) -' (G .order() ))) by A2, Th14
.= (Seg (G .order() )) \ (Seg 0 ) by XREAL_1:234
.= Seg (G .order() ) ;
then dom ((((LexBFS:CSeq G) . (G .order() )) `1 ) " ) = Seg (G .order() ) by A3, A4, FUNCT_1:55;
then (((LexBFS:CSeq G) . (G .order() )) `1 ) " is FinSequence by FINSEQ_1:def 2;
then (((LexBFS:CSeq G) . (G .order() )) `1 ) " is FinSequence of the_Vertices_of G by A5, FINSEQ_1:def 4;
hence (((LexBFS:CSeq G) .Result() ) `1 ) " is VertexScheme of G by A1, A4, A5, CHORD:def 12; :: thesis: verum