for G being _finite connected real-weighted WGraph holds (PRIM:MST G) `1 = the_Vertices_of G