:: deftheorem Def16 defines LexBFS:CSeq LEXBFS:def 17 :
for G being _finite _Graph
for b₂ being LexBFS:LabelingSeq of G holds
( b₂ = LexBFS:CSeq G iff ( b₂ . 0 = LexBFS:Init G & ( for n being Nat holds b₂ . (n + 1) = LexBFS:Step (b₂ . n) ) ) );