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 VNS0
.= ((LexBFS:CSeq G) .Result() ) `1 by d1stBFSLS ; :: thesis: verum