let G be finite connected real-weighted WGraph; :: thesis: (PRIM:MST G) `1 = the_Vertices_of G
set M = PRIM:MST G;
set PCS = PRIM:CompSeq G;
set V = (PRIM:MST G) `1 ;
set src = choose (the_Vertices_of G);
set RFS = G .reachableFrom (choose (the_Vertices_of G));
((PRIM:CompSeq G) .Lifespan() ) + 1 = card (G .reachableFrom (choose (the_Vertices_of G))) by Lm16;
then A1: card ((PRIM:MST G) `1 ) = min (card (G .reachableFrom (choose (the_Vertices_of G)))),(card (G .reachableFrom (choose (the_Vertices_of G)))) by Lm15;
A2: (PRIM:MST G) `1 c= G .reachableFrom (choose (the_Vertices_of G)) by Lm12;

now

assume (PRIM:MST G) `1 <> G .reachableFrom (choose (the_Vertices_of G)) ; :: thesis: contradiction
then (PRIM:MST G) `1 c< G .reachableFrom (choose (the_Vertices_of G)) by A2, XBOOLE_0:def 8;
hence contradiction by A1, CARD_2:67; :: thesis: verum

end;

hence (PRIM:MST G) `1 = the_Vertices_of G by GLIB_002:16; :: thesis: verum