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 Th37;
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 Th36;
A2: (PRIM:MST G) `1 c= G .reachableFrom (choose (the_Vertices_of G)) by Th33;

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:48; :: thesis: verum

end;

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