:: deftheorem Def13 defines PRIM:NextBestEdges GLIB_004:def 13 :
for G being real-weighted WGraph
for L being PRIM:Labeling of G
for b₃ being Subset of (the_Edges_of G) holds
( b₃ = PRIM:NextBestEdges L iff for e1 being set holds
( e1 in b₃ iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) );