let G be real-weighted WGraph; :: thesis: for L being PRIM:Labeling of G holds
( L `1 c= (PRIM:Step L) `1 & L `2 c= (PRIM:Step L) `2 )
let L be PRIM:Labeling of G; :: thesis: ( L `1 c= (PRIM:Step L) `1 & L `2 c= (PRIM:Step L) `2 )
set G2 = PRIM:Step L;
set Next = PRIM:NextBestEdges L;
set e = choose (PRIM:NextBestEdges L);
set GE = L \/ {(choose (PRIM:NextBestEdges L))};

now

per cases ( PRIM:NextBestEdges L = {} or PRIM:NextBestEdges L <> {} ) ;

suppose PRIM:NextBestEdges L = {} ; :: thesis: ( L `1 c= (PRIM:Step L) `1 & L `2 c= (PRIM:Step L) `2 )

hence ( L `1 c= (PRIM:Step L) `1 & L `2 c= (PRIM:Step L) `2 ) by Def15; :: thesis: verum

end;

suppose PRIM:NextBestEdges L <> {} ; :: thesis: ( L `1 c= (PRIM:Step L) `1 & L `2 c= (PRIM:Step L) `2 )

then consider v being Vertex of G such that
not v in L `1 and
A1: PRIM:Step L = [((L `1 ) \/ {v}),((L `2 ) \/ {(choose (PRIM:NextBestEdges L))})] by Th28;
(PRIM:Step L) `1 = (L `1 ) \/ {v} by A1, MCART_1:7;
hence L `1 c= (PRIM:Step L) `1 by XBOOLE_1:7; :: thesis: L `2 c= (PRIM:Step L) `2
(PRIM:Step L) `2 = (L `2 ) \/ {(choose (PRIM:NextBestEdges L))} by A1, MCART_1:7;
hence L `2 c= (PRIM:Step L) `2 by XBOOLE_1:7; :: thesis: verum

end;

end;

end;

hence ( L `1 c= (PRIM:Step L) `1 & L `2 c= (PRIM:Step L) `2 ) ; :: thesis: verum