theorem Th32: :: LEXBFS:32

for G being _finite _Graph
for n being Nat st n <= G .order() holds
card (dom (((LexBFS:CSeq G) . n) `1)) = n