let G be finite connected real-weighted WGraph; :: thesis: for n being Nat holds ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2
let n be Nat; :: thesis: ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2
set PCS = PRIM:CompSeq G;
defpred S₁[ Nat] means (PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + $1) = PRIM:MST G;

A1: now

set off = (PRIM:CompSeq G) .Lifespan() ;
let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set Gn = (PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + n);
set Gn1 = (PRIM:CompSeq G) . ((((PRIM:CompSeq G) .Lifespan() ) + n) + 1);
set Next = PRIM:NextBestEdges ((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + n));
set e = choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + n)));
A2: (PRIM:CompSeq G) . ((((PRIM:CompSeq G) .Lifespan() ) + n) + 1) = PRIM:Step ((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + n)) by Def17;
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
then A4: ((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + n)) `1 = the_Vertices_of G by Th39;

now

assume PRIM:NextBestEdges ((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + n)) <> {} ; :: thesis: contradiction
then ex v being Vertex of G st
( not v in ((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + n)) `1 & (PRIM:CompSeq G) . ((((PRIM:CompSeq G) .Lifespan() ) + n) + 1) = [((((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + n)) `1 ) \/ {v}),((((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + n)) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan() ) + n))))})] ) by A2, Th28;
hence contradiction by A4; :: thesis: verum

end;

hence S₁[n + 1] by A3, A2, Def15; :: thesis: verum

end;

A5: S₁[ 0 ] ;
A6: for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A1);

now

per cases ( n <= (PRIM:CompSeq G) .Lifespan() or (PRIM:CompSeq G) .Lifespan() < n ) ;

suppose n <= (PRIM:CompSeq G) .Lifespan() ; :: thesis: ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2

hence ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2 by Th34; :: thesis: verum

end;

suppose (PRIM:CompSeq G) .Lifespan() < n ; :: thesis: ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2

then ex k being Nat st n = ((PRIM:CompSeq G) .Lifespan() ) + k by NAT_1:10;
hence ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2 by A6; :: thesis: verum

end;

end;

end;

hence ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2 ; :: thesis: verum