:: deftheorem Def16 defines PRIM:LabelingSeq GLIB_004:def 16 :
for G being real-weighted WGraph
for b₂ being ManySortedSet of NAT holds
( b₂ is PRIM:LabelingSeq of G iff for n being Nat holds b₂ . n is PRIM:Labeling of G );