let G1 be _Graph; :: thesis: for E being Subset of ()
for G2 being inducedSubgraph of G1, the_Vertices_of G1,E st G2 is connected holds
G1 is connected

let E be Subset of (); :: thesis: for G2 being inducedSubgraph of G1, the_Vertices_of G1,E st G2 is connected holds
G1 is connected

let G2 be inducedSubgraph of G1, the_Vertices_of G1,E; :: thesis: ( G2 is connected implies G1 is connected )
assume A1: G2 is connected ; :: thesis: G1 is connected
now :: thesis: for v1, w1 being Vertex of G1 ex W1 being Walk of G1 st W1 is_Walk_from v1,w1
let v1, w1 be Vertex of G1; :: thesis: ex W1 being Walk of G1 st W1 is_Walk_from v1,w1
E c= the_Edges_of G1 ;
then ( E c= G1 .edgesBetween () & the_Vertices_of G1 c= the_Vertices_of G1 ) by GLIB_000:34;
then reconsider v2 = v1, w2 = w1 as Vertex of G2 by GLIB_000:def 37;
consider W2 being Walk of G2 such that
A2: W2 is_Walk_from v2,w2 by ;
reconsider W1 = W2 as Walk of G1 by GLIB_001:167;
take W1 = W1; :: thesis: W1 is_Walk_from v1,w1
thus W1 is_Walk_from v1,w1 by ; :: thesis: verum
end;
hence G1 is connected by GLIB_002:def 1; :: thesis: verum