for G being _finite real-weighted WGraph
for n being Nat holds
( ((PRIM:CompSeq G) . n) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . n) `2 c= G .edgesBetween (((PRIM:CompSeq G) . n) `1) )