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 Def15;
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:33;
(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:232
.= Seg (G .order()) ;
then dom ((((LexBFS:CSeq G) . (G .order())) `1) ") = Seg (G .order()) by A3, A4, FUNCT_1:33;
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