theorem Th37: :: LEXBFS:37

for G being _finite _Graph holds (LexBFS:CSeq G) .Lifespan() = G .order()