for G being _finite _Graph
for x being set
for i, j being Nat st i <= j holds
(((LexBFS:CSeq G) . i) `2) . x c= (((LexBFS:CSeq G) . j) `2) . x