:: deftheorem Def7 defines DIJK:NextBestEdges GLIB_004:def 7 :
for G being real-weighted WGraph
for L being DIJK:Labeling of G
for b₃ being Subset of (the_Edges_of G) holds
( b₃ = DIJK:NextBestEdges L iff for e1 being set holds
( e1 in b₃ iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds
((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) );