let G1 be _Graph; :: thesis: for G2 being connected Subgraph of G1 st G2 is spanning holds
G1 is connected
let G2 be connected Subgraph of G1; :: thesis: ( G2 is spanning implies G1 is connected )
assume A1: G2 is spanning ; :: thesis: G1 is connected

now :: thesis: for u9, v9 being Vertex of G1 ex W being Walk of G1 st W is_Walk_from u9,v9

let u9, v9 be Vertex of G1; :: thesis: ex W being Walk of G1 st W is_Walk_from u9,v9
reconsider u = u9, v = v9 as Vertex of G2 by A1, GLIB_000:def 33;
consider W being Walk of G2 such that
A2: W is_Walk_from u,v by Def1;
reconsider W = W as Walk of G1 by GLIB_001:167;
take W = W; :: thesis: W is_Walk_from u9,v9
thus W is_Walk_from u9,v9 by A2, GLIB_001:19; :: thesis: verum

end;

hence G1 is connected ; :: thesis: verum