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

now

let u, v be Vertex of ; :: thesis: ex W being Walk of G2 st W is_Walk_from u,v
reconsider u' = u, v' = v as Vertex of by A1, GLIB_000:def 36;
consider W' being Walk of G1 such that
A3: W' is_Walk_from u',v' by A2, 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 A3, GLIB_001:20; :: thesis: verum

end;

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