for G being real-weighted WGraph
for L being PRIM:Labeling of G holds
( L `1 c= (PRIM:Step L) `1 & L `2 c= (PRIM:Step L) `2 )