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