for G being _finite _Graph
for n being Nat holds ((LexBFS:CSeq G) . n) `1 is with_property_L3