theorem Th28: :: LEXBFS:28

for G being finite _Graph holds LexBFS:CSeq G is iterative