theorem Th36: :: LEXBFS:36

for G being finite _Graph
for n being Nat holds
( dom (((LexBFS:CSeq G) . n) `1) = the_Vertices_of G iff G .order() <= n )