for G being _finite _Graph
for i, j being Nat
for a, b being Vertex of G st a in dom (((LexBFS:CSeq G) . i) `1) & b in dom (((LexBFS:CSeq G) . i) `1) & (((LexBFS:CSeq G) . i) `1) . a < (((LexBFS:CSeq G) . i) `1) . b & j = (G .order()) -' ((((LexBFS:CSeq G) . i) `1) . b) holds
(((((LexBFS:CSeq G) . j) `2) . a),1) -bag <= (((((LexBFS:CSeq G) . j) `2) . b),1) -bag , InvLexOrder NAT