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