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

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

hence
G1 is connected
by GLIB_002:def 1; :: thesis: verumlet 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;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