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 Def15 ; :: thesis: verum