for G being _finite real-weighted WGraph
for n being Nat holds ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the Element of the_Vertices_of G