theorem Th30: :: GLIB_004:30

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) )