let G be real-weighted WGraph; :: thesis: 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})] )
let L be PRIM:Labeling of G; :: thesis: ( PRIM:NextBestEdges L <> {} implies 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})] ) )
set G2 = PRIM:Step L;
set e = the Element of PRIM:NextBestEdges L;
set src = (the_Source_of G) . the Element of PRIM:NextBestEdges L;
set tar = (the_Target_of G) . the Element of PRIM:NextBestEdges L;
assume A1: PRIM:NextBestEdges L <> {} ; :: thesis: 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})] )
then the Element of PRIM:NextBestEdges L in PRIM:NextBestEdges L ;
then reconsider src = (the_Source_of G) . the Element of PRIM:NextBestEdges L, tar = (the_Target_of G) . the Element of PRIM:NextBestEdges L as Vertex of G by FUNCT_2:5;
A2: the Element of PRIM:NextBestEdges L SJoins L `1 ,(the_Vertices_of G) \ (L `1),G by A1, Def13;

now :: thesis: ex tar being Vertex of G st
( not tar in L `1 & PRIM:Step L = [((L `1) \/ {tar}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] )

per cases ( src in L `1 or not src in L `1 ) ;

suppose A3: src in L `1 ; :: thesis: ex tar being Vertex of G st
( not tar in L `1 & PRIM:Step L = [((L `1) \/ {tar}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] )

take tar = tar; :: thesis: ( not tar in L `1 & PRIM:Step L = [((L `1) \/ {tar}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] )
not src in (the_Vertices_of G) \ (L `1) by A3, XBOOLE_0:def 5;
then tar in (the_Vertices_of G) \ (L `1) by A2;
hence not tar in L `1 by XBOOLE_0:def 5; :: thesis: PRIM:Step L = [((L `1) \/ {tar}),((L `2) \/ { the Element of PRIM:NextBestEdges L})]
thus PRIM:Step L = [((L `1) \/ {tar}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] by A1, A3, Def15; :: thesis: verum

end;

suppose A4: not src in L `1 ; :: thesis: ex src being Vertex of G st
( not src in L `1 & PRIM:Step L = [((L `1) \/ {src}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] )

take src = src; :: thesis: ( not src in L `1 & PRIM:Step L = [((L `1) \/ {src}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] )
thus not src in L `1 by A4; :: thesis: PRIM:Step L = [((L `1) \/ {src}),((L `2) \/ { the Element of PRIM:NextBestEdges L})]
thus PRIM:Step L = [((L `1) \/ {src}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] by A1, A4, Def15; :: thesis: verum

end;

end;

end;

hence 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})] ) ; :: thesis: verum