set V = the_Vertices_of G;
set E = the_Edges_of G;
set BE = PRIM:NextBestEdges L;
set e = the Element of PRIM:NextBestEdges L;
set s = (the_Source_of G) . the Element of PRIM:NextBestEdges L;
set t = (the_Target_of G) . the Element of PRIM:NextBestEdges L;

A1: now :: thesis:

assume that
A2: PRIM:NextBestEdges L <> {} and
not (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 ; :: thesis:
the Element of PRIM:NextBestEdges L in PRIM:NextBestEdges L by A2;
then reconsider s9 = (the_Source_of G) . the Element of PRIM:NextBestEdges L as Element of the_Vertices_of G by FUNCT_2:5;
A3: (L `1) \/ {s9} c= the_Vertices_of G ;
A4: { the Element of PRIM:NextBestEdges L} c= the_Edges_of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { the Element of PRIM:NextBestEdges L} ; :: thesis:
then x = the Element of PRIM:NextBestEdges L by TARSKI:def 1;
then x in PRIM:NextBestEdges L by A2;
hence x in the_Edges_of G ; :: thesis:

end;

(L `2) \/ { the Element of PRIM:NextBestEdges L} c= the_Edges_of G by A4, XBOOLE_1:8;
hence [((L `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] is PRIM:Labeling of G by A3, ZFMISC_1:def 2; :: thesis:

end;

now :: thesis:

assume that
A5: PRIM:NextBestEdges L <> {} and
(the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 ; :: thesis:
the Element of PRIM:NextBestEdges L in PRIM:NextBestEdges L by A5;
then reconsider t9 = (the_Target_of G) . the Element of PRIM:NextBestEdges L as Element of the_Vertices_of G by FUNCT_2:5;
A6: (L `1) \/ {t9} c= the_Vertices_of G ;
A7: { the Element of PRIM:NextBestEdges L} c= the_Edges_of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { the Element of PRIM:NextBestEdges L} ; :: thesis:
then x = the Element of PRIM:NextBestEdges L by TARSKI:def 1;
then x in PRIM:NextBestEdges L by A5;
hence x in the_Edges_of G ; :: thesis:

end;

(L `2) \/ { the Element of PRIM:NextBestEdges L} c= the_Edges_of G by A7, XBOOLE_1:8;
hence [((L `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] is PRIM:Labeling of G by A6, ZFMISC_1:def 2; :: thesis:

end;

hence ( ( PRIM:NextBestEdges L = {} implies L is PRIM:Labeling of G ) & ( PRIM:NextBestEdges L <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 implies [((L `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] is PRIM:Labeling of G ) & ( not PRIM:NextBestEdges L = {} & ( not PRIM:NextBestEdges L <> {} or not (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 ) implies [((L `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] is PRIM:Labeling of G ) ) by A1; :: thesis: