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

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

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