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

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

hence
G1 is connected
; :: thesis: verumlet 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;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