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

A1: now

assume that
A2: PRIM:NextBestEdges L <> {} and
not (the_Source_of G) . (choose (PRIM:NextBestEdges L)) in L `1 ; :: thesis: [((L `1) \/ {((the_Source_of G) . (choose (PRIM:NextBestEdges L)))}),((L `2) \/ {(choose (PRIM:NextBestEdges L))})] is PRIM:Labeling of G
choose (PRIM:NextBestEdges L) in PRIM:NextBestEdges L by A2;
then reconsider s9 = (the_Source_of G) . (choose (PRIM:NextBestEdges L)) as Element of the_Vertices_of G by FUNCT_2:5;
L `1 in bool (the_Vertices_of G) by MCART_1:10;
then A3: (L `1) \/ {s9} c= the_Vertices_of G by XBOOLE_1:8;
A4: {(choose (PRIM:NextBestEdges L))} c= the_Edges_of G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(choose (PRIM:NextBestEdges L))} or x in the_Edges_of G )
assume x in {(choose (PRIM:NextBestEdges L))} ; :: thesis: x in the_Edges_of G
then x = choose (PRIM:NextBestEdges L) by TARSKI:def 1;
then x in PRIM:NextBestEdges L by A2;
hence x in the_Edges_of G ; :: thesis: verum

end;

L `2 in bool (the_Edges_of G) by MCART_1:10;
then (L `2) \/ {(choose (PRIM:NextBestEdges L))} c= the_Edges_of G by A4, XBOOLE_1:8;
hence [((L `1) \/ {((the_Source_of G) . (choose (PRIM:NextBestEdges L)))}),((L `2) \/ {(choose (PRIM:NextBestEdges L))})] is PRIM:Labeling of G by A3, ZFMISC_1:def 2; :: thesis: verum

end;

now

assume that
A5: PRIM:NextBestEdges L <> {} and
(the_Source_of G) . (choose (PRIM:NextBestEdges L)) in L `1 ; :: thesis: [((L `1) \/ {((the_Target_of G) . (choose (PRIM:NextBestEdges L)))}),((L `2) \/ {(choose (PRIM:NextBestEdges L))})] is PRIM:Labeling of G
choose (PRIM:NextBestEdges L) in PRIM:NextBestEdges L by A5;
then reconsider t9 = (the_Target_of G) . (choose (PRIM:NextBestEdges L)) as Element of the_Vertices_of G by FUNCT_2:5;
L `1 in bool (the_Vertices_of G) by MCART_1:10;
then A6: (L `1) \/ {t9} c= the_Vertices_of G by XBOOLE_1:8;
A7: {(choose (PRIM:NextBestEdges L))} c= the_Edges_of G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(choose (PRIM:NextBestEdges L))} or x in the_Edges_of G )
assume x in {(choose (PRIM:NextBestEdges L))} ; :: thesis: x in the_Edges_of G
then x = choose (PRIM:NextBestEdges L) by TARSKI:def 1;
then x in PRIM:NextBestEdges L by A5;
hence x in the_Edges_of G ; :: thesis: verum

end;

L `2 in bool (the_Edges_of G) by MCART_1:10;
then (L `2) \/ {(choose (PRIM:NextBestEdges L))} c= the_Edges_of G by A7, XBOOLE_1:8;
hence [((L `1) \/ {((the_Target_of G) . (choose (PRIM:NextBestEdges L)))}),((L `2) \/ {(choose (PRIM:NextBestEdges L))})] is PRIM:Labeling of G by A6, ZFMISC_1:def 2; :: thesis: verum

end;

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