theorem Th49: :: LEXBFS:49
for G being _finite _Graph holds dom (((LexBFS:CSeq G) .Result()) `1) = the_Vertices_of G