let G be finite _Graph; :: thesis: ((LexBFS:CSeq G) ``1 ) .Result() = ((LexBFS:CSeq G) .Result() ) `1
set S = LexBFS:CSeq G;
thus ((LexBFS:CSeq G) ``1 ) .Result() = ((LexBFS:CSeq G) ``1 ) . ((LexBFS:CSeq G) .Lifespan() ) by Th39
.= ((LexBFS:CSeq G) .Result() ) `1 by Def16 ; :: thesis: verum