theorem Th70: :: LEXBFS:70

for G being finite _Graph holds (MCS:CSeq G) .Lifespan() = G .order()