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