:: deftheorem Def24 defines ``1 LEXBFS:def 25 :
for G being _finite _Graph
for S being MCS:LabelingSeq of G
for b<sub>3</sub> being preVNumberingSeq of G holds
( b<sub>3</sub> = S ``1 iff for n being Nat holds b₃ . n = (S . n) `1 );