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 ;
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 Th30;
set E = ((PRIM:CompSeq G1) . n) `2 ;
reconsider E = ((PRIM:CompSeq G1) . n) `2 as Subset of (G1 .edgesBetween V) by Th30;
set G3 = the inducedSubgraph of G1,V,E;
A1: ( the_Vertices_of the inducedSubgraph of G1,V,E = V & the_Vertices_of G2 = V ) by GLIB_000:def 37;
( the_Edges_of the inducedSubgraph of G1,V,E = E & the_Edges_of G2 = G1 .edgesBetween V ) by GLIB_000:def 37;
then reconsider G3 = the inducedSubgraph of G1,V,E as Subgraph of G2 by A1, GLIB_000:44;
A2: G3 is spanning by A1;
G3 is connected by Th31;
hence G2 is connected by A2, GLIB_002:23; :: thesis: verum