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 :: thesis: for u, v being Vertex of G2 ex W being Walk of G2 st W is_Walk_from u,v
let u, v be Vertex of G2; :: thesis: ex W being Walk of G2 st W is_Walk_from u,v
reconsider u9 = u, v9 = v as Vertex of G1 by A1, GLIB_000:def 34;
consider W9 being Walk of G1 such that
A3: W9 is_Walk_from u9,v9 by A2;
reconsider W = W9 as Walk of G2 by A1, GLIB_001:179;
take W = W; :: thesis: W is_Walk_from u,v
thus W is_Walk_from u,v by A3, GLIB_001:19; :: thesis: verum
end;
hence G2 is connected ; :: thesis: verum