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 = the Element of the_Vertices_of G;
set RFS = G .reachableFrom the Element of the_Vertices_of G;
((PRIM:CompSeq G) .Lifespan()) + 1 = card (G .reachableFrom the Element of the_Vertices_of G) by Th37;
then A1: card ((PRIM:MST G) `1) = min ((card (G .reachableFrom the Element of the_Vertices_of G)),(card (G .reachableFrom the Element of the_Vertices_of G))) by Th36;
A2: (PRIM:MST G) `1 c= G .reachableFrom the Element of the_Vertices_of G by Th33;

now :: thesis: not (PRIM:MST G) `1 <> G .reachableFrom the Element of the_Vertices_of G

assume (PRIM:MST G) `1 <> G .reachableFrom the Element of the_Vertices_of G ; :: thesis: contradiction
then (PRIM:MST G) `1 c< G .reachableFrom the Element of 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