theorem Th28: :: GLIB_004:28

for G being real-weighted WGraph
for L being PRIM:Labeling of G st PRIM:NextBestEdges L <> {} holds
ex v being Vertex of G st
( not v in L `1 & PRIM:Step L = [((L `1) \/ {v}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] )