let G1 be finite real-weighted WGraph; :: thesis: for n being Nat
for G2 being inducedSubgraph of G1,(((PRIM:CompSeq G1) . n) `1 ) holds G2 is connected
let n be Nat; :: thesis: for G2 being inducedSubgraph of G1,(((PRIM:CompSeq G1) . n) `1 ) holds G2 is connected
set V = ((PRIM:CompSeq G1) . n) `1 ;
set E = ((PRIM:CompSeq G1) . n) `2 ;
let G2 be inducedSubgraph of G1,(((PRIM:CompSeq G1) . n) `1 ); :: thesis: G2 is connected
reconsider V = ((PRIM:CompSeq G1) . n) `1 as non empty Subset of (the_Vertices_of G1) by Lm9;
reconsider E = ((PRIM:CompSeq G1) . n) `2 as Subset of (G1 .edgesBetween V) by Lm9;
consider G3 being inducedSubgraph of G1,V,E;
A1: ( the_Vertices_of G3 = V & the_Edges_of G3 = E ) by GLIB_000:def 39;
A2: ( the_Vertices_of G2 = V & the_Edges_of G2 = G1 .edgesBetween V ) by GLIB_000:def 39;
then reconsider G3 = G3 as Subgraph of G2 by A1, GLIB_000:47;
A3: G3 is connected by Lm10;
G3 is spanning by A1, A2, GLIB_000:def 35;
hence G2 is connected by A3, GLIB_002:23; :: thesis: verum