for G1 being _finite real-weighted WGraph
for n being Nat
for G2 being inducedSubgraph of G1,(((PRIM:CompSeq G1) . n) `1) holds G2 is connected