let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is connected implies G2 is connected )
assume A1: ( G1 == G2 & G1 is connected ) ; :: thesis: G2 is connected

now

let u, v be Vertex of G2; :: thesis: ex W being Walk of G2 st W is_Walk_from u,v
reconsider u' = u, v' = v as Vertex of G1 by A1, GLIB_000:def 36;
consider W' being Walk of G1 such that
A2: W' is_Walk_from u',v' by A1, Def1;
reconsider W = W' as Walk of G2 by A1, GLIB_001:180;
take W = W; :: thesis: W is_Walk_from u,v
thus W is_Walk_from u,v by A2, GLIB_001:20; :: thesis: verum

end;

hence G2 is connected by Def1; :: thesis: verum