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

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

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