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

now :: thesis: for v2, w2 being Vertex of G2 ex W2 being Walk of G2 st W2 is_Walk_from v2,w2

let v2, w2 be Vertex of G2; :: thesis: ex W2 being Walk of G2 st W2 is_Walk_from v2,w2
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: W2 is_Walk_from v2,w2
thus W2 is_Walk_from v2,w2 by A4; :: thesis: verum

end;

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