theorem Th72: :: LEXBFS:72

for G being _finite _Graph holds ((MCS:CSeq G) ``1) .Lifespan() = (MCS:CSeq G) .Lifespan()