let G1 be _Graph; :: thesis:
let G2 be Subgraph of G1; :: thesis:
assume A1: for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() ; :: thesis:
assume A2: G1 is connected ; :: thesis:

now :: thesis:

let v2, w2 be Vertex of G2; :: thesis:
the_Vertices_of G2 c= the_Vertices_of G1 ;
then reconsider v1 = v2, w1 = w2 as Vertex of G1 by TARSKI:def 3;
consider W1 being Walk of G1 such that
A3: W1 is_Walk_from v1,w1 by A2, GLIB_002:def 1;
( W1 .first() = v1 & W1 .last() = w1 ) by A3, GLIB_001:def 23;
then consider W2 being Walk of G2 such that
A4: W2 is_Walk_from v1,w1 by A1;
take W2 = W2; :: thesis:
thus W2 is_Walk_from v2,w2 by A4; :: thesis:

end;

hence G2 is connected by GLIB_002:def 1; :: thesis: