:: deftheorem Def8 defines DIJK:Step GLIB_004:def 8 :
for G being real-weighted WGraph
for L being DIJK:Labeling of G holds
( ( DIJK:NextBestEdges L = {} implies DIJK:Step L = L ) & ( not DIJK:NextBestEdges L = {} implies DIJK:Step L = [((L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L)))),((L `2) \/ { the Element of DIJK:NextBestEdges L})] ) );