let G1 be _Graph; :: thesis: for E being Subset of (the_Edges_of G1)
for G2 being inducedSubgraph of G1, the_Vertices_of G1,E st G2 is connected holds
G1 is connected
let E be Subset of (the_Edges_of G1); :: 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) & 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 A1, GLIB_002:def 1;
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 A2, GLIB_001:19; :: thesis: verum

end;

hence G1 is connected by GLIB_002:def 1; :: thesis: verum