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

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