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 ;
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 A1: 0 + 1 <= card (G .reachableFrom (choose (the_Vertices_of G))) by CARD_1:50;

A2: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: 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));
A4: (PRIM:CompSeq G) . (n + 1) = PRIM:Step ((PRIM:CompSeq G) . n) by Def17;

now

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

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

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

end;

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

A9: ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom (choose (the_Vertices_of G)) by Th33;
A10: ((PRIM:CompSeq G) . n) `1 <> G .reachableFrom (choose (the_Vertices_of G)) by A8, Th35;

A11: now

assume A12: 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 A10, A9, XBOOLE_0:def 8;
hence contradiction by A12, CARD_2:67; :: thesis: verum

end;

then A13: card (((PRIM:CompSeq G) . n) `1 ) = n + 1 by A3, XXREAL_0:15;
consider v being Vertex of G such that
A14: not v in ((PRIM:CompSeq G) . n) `1 and
A15: (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1 ) \/ {v}),((((PRIM:CompSeq G) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))})] by A4, A8, Th28;
A16: card (((PRIM:CompSeq G) . (n + 1)) `1 ) = card ((((PRIM:CompSeq G) . n) `1 ) \/ {v}) by A15, MCART_1:7
.= (card (((PRIM:CompSeq G) . n) `1 )) + 1 by A14, CARD_2:54 ;
card (((PRIM:CompSeq G) . n) `1 ) <= card (G .reachableFrom (choose (the_Vertices_of G))) by Th33, NAT_1:44;
then n + 1 < card (G .reachableFrom (choose (the_Vertices_of G))) by A11, A13, XXREAL_0:1;
then (n + 1) + 1 <= card (G .reachableFrom (choose (the_Vertices_of G))) by NAT_1:13;
hence S₁[n + 1] by A16, A13, XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

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

end;

(PRIM:CompSeq G) . 0 = PRIM:Init G by Def17;
then {(choose (the_Vertices_of G))} = ((PRIM:CompSeq G) . 0 ) `1 by MCART_1:7;
then card (((PRIM:CompSeq G) . 0 ) `1 ) = 1 by CARD_1:50;
then A17: S₁[ 0 ] by A1, XXREAL_0:def 9;
for n being Nat holds S₁[n] from NAT_1:sch 2(A17, A2);
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