let G1 be _Graph; :: thesis:
let G2 be connected Subgraph of G1; :: thesis:
assume A1: G2 is spanning ; :: thesis:

now :: thesis:

let u9, v9 be Vertex of G1; :: thesis:
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:
thus W is_Walk_from u9,v9 by A2, GLIB_001:19; :: thesis:

end;

hence G1 is connected ; :: thesis: