let G be finite real-weighted WGraph; :: thesis: for n being Nat holds card (((PRIM:CompSeq G) . n) `1 ) = min (n + 1),(card (G .reachableFrom (choose (the_Vertices_of G))))
set CS = PRIM:CompSeq G;
set src = choose (the_Vertices_of G);
defpred S<sub>1</sub>[ Nat] means card (((PRIM:CompSeq G) . $1) `1 ) = min ($1 + 1),(card (G .reachableFrom (choose (the_Vertices_of G))));
set G0 = (PRIM:CompSeq G) . 0 ;
(PRIM:CompSeq G) . 0 = PRIM:Init G by Def15;
then {(choose (the_Vertices_of G))} = ((PRIM:CompSeq G) . 0 ) `1 by MCART_1:7;
then A1: card (((PRIM:CompSeq G) . 0 ) `1 ) = 1 by CARD_1:50;
choose (the_Vertices_of G) in G .reachableFrom (choose (the_Vertices_of G)) by GLIB_002:9;
then {(choose (the_Vertices_of G))} c= G .reachableFrom (choose (the_Vertices_of G)) by ZFMISC_1:37;
then card {(choose (the_Vertices_of G))} <= card (G .reachableFrom (choose (the_Vertices_of G))) by NAT_1:44;
then 0 + 1 <= card (G .reachableFrom (choose (the_Vertices_of G))) by CARD_1:50;
then A2: S₁[ 0 ] by A1, XXREAL_0:def 9;

A3: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set Gn = (PRIM:CompSeq G) . n;
set Gn1 = (PRIM:CompSeq G) . (n + 1);
set e = choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n));
A5: (PRIM:CompSeq G) . (n + 1) = PRIM:Step ((PRIM:CompSeq G) . n) by Def15;

now

per cases ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} or PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} ) ;

suppose A6: PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} ; :: thesis: S₁[n + 1]

then A7: card (((PRIM:CompSeq G) . (n + 1)) `1 ) = min (n + 1),(card (G .reachableFrom (choose (the_Vertices_of G)))) by A4, A5, Def14;
A8: card (((PRIM:CompSeq G) . n) `1 ) = card (G .reachableFrom (choose (the_Vertices_of G))) by A6, Lm14;
then card (G .reachableFrom (choose (the_Vertices_of G))) <= n + 1 by A4, XXREAL_0:def 9;
then card (G .reachableFrom (choose (the_Vertices_of G))) <= (n + 1) + 1 by NAT_1:12;
hence S₁[n + 1] by A4, A7, A8, XXREAL_0:def 9; :: thesis: verum

end;

suppose A9: PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} ; :: thesis: S₁[n + 1]

then consider v being Vertex of G such that
A10: ( not v in ((PRIM:CompSeq G) . n) `1 & (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1 ) \/ {v}),((((PRIM:CompSeq G) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))})] ) by A5, Lm6;
A12: card (((PRIM:CompSeq G) . (n + 1)) `1 ) = card ((((PRIM:CompSeq G) . n) `1 ) \/ {v}) by A10, MCART_1:7
.= (card (((PRIM:CompSeq G) . n) `1 )) + 1 by A10, CARD_2:54 ;
A13: ((PRIM:CompSeq G) . n) `1 <> G .reachableFrom (choose (the_Vertices_of G)) by A9, Lm14;
A14: ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom (choose (the_Vertices_of G)) by Lm12;
A15: card (((PRIM:CompSeq G) . n) `1 ) <= card (G .reachableFrom (choose (the_Vertices_of G))) by Lm12, NAT_1:44;

A16: now

assume A17: card (((PRIM:CompSeq G) . n) `1 ) = card (G .reachableFrom (choose (the_Vertices_of G))) ; :: thesis: contradiction
((PRIM:CompSeq G) . n) `1 c< G .reachableFrom (choose (the_Vertices_of G)) by A13, A14, XBOOLE_0:def 8;
hence contradiction by A17, CARD_2:67; :: thesis: verum

end;

then A18: card (((PRIM:CompSeq G) . n) `1 ) = n + 1 by A4, XXREAL_0:15;
then n + 1 < card (G .reachableFrom (choose (the_Vertices_of G))) by A15, A16, XXREAL_0:1;
then (n + 1) + 1 <= card (G .reachableFrom (choose (the_Vertices_of G))) by NAT_1:13;
hence S₁[n + 1] by A12, A18, XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence for n being Nat holds card (((PRIM:CompSeq G) . n) `1 ) = min (n + 1),(card (G .reachableFrom (choose (the_Vertices_of G)))) ; :: thesis: verum