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 S1[ Nat] means (PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan()) + $1) = PRIM:MST G;
A1: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
set off = (PRIM:CompSeq G) .Lifespan() ;
let n be Nat; :: thesis: ( S1[n] implies S1[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 = the Element of 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: S1[n] ; :: thesis: S1[n + 1]
then A4: ((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan()) + n)) `1 = the_Vertices_of G by Th39;
now :: thesis: not PRIM:NextBestEdges ((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan()) + n)) <> {}
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) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . (((PRIM:CompSeq G) .Lifespan()) + n))})] ) by A2, Th28;
hence contradiction by A4; :: thesis: verum
end;
hence S1[n + 1] by A3, A2, Def15; :: thesis: verum
end;
A5: S1[ 0 ] ;
A6: for n being Nat holds S1[n] from NAT_1:sch 2(A5, A1);
now :: thesis: ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2
per cases ( n <= (PRIM:CompSeq G) .Lifespan() or (PRIM:CompSeq G) .Lifespan() < n ) ;
end;
end;
hence ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2 ; :: thesis: verum