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