:: deftheorem Def23 defines MCS:LabelingSeq LEXBFS:def 24 :
for G being _Graph
for b₂ being ManySortedSet of NAT holds
( b₂ is MCS:LabelingSeq of G iff for n being Nat holds b₂ . n is MCS:Labeling of G );