theorem Th39: :: LEXBFS:39

for G being finite _Graph holds ((LexBFS:CSeq G) ``1) .Lifespan() = (LexBFS:CSeq G) .Lifespan()