:: deftheorem Def15 defines PRIM:Step GLIB_004:def 15 :
for G being real-weighted WGraph
for L being PRIM:Labeling of G holds
( ( PRIM:NextBestEdges L = {} implies PRIM:Step L = L ) & ( PRIM:NextBestEdges L <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 implies PRIM:Step L = [((L `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] ) & ( not PRIM:NextBestEdges L = {} & ( not PRIM:NextBestEdges L <> {} or not (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 ) implies PRIM:Step L = [((L `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] ) );