theorem Th56: :: LEXBFS:56

for G being _finite _Graph holds MCS:CSeq G is iterative