theorem Th36: :: GLIB_004:36

for G being finite real-weighted WGraph
for n being Nat holds card (((PRIM:CompSeq G) . n) `1) = min ((n + 1),(card (G .reachableFrom the Element of the_Vertices_of G)))