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 = the Element of PRIM:NextBestEdges L;

now :: thesis: ( L `1 c= (PRIM:Step L) `1 & L `2 c= (PRIM:Step L) `2 )

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) \/ { the Element of PRIM:NextBestEdges L})] by Th28;
(PRIM:Step L) `1 = (L `1) \/ {v} by A1;
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) \/ { the Element of PRIM:NextBestEdges L} by A1;
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