let G1, G2 be connected _Graph; :: thesis: for G being GraphUnion of G1,G2 st the_Vertices_of G1 meets the_Vertices_of G2 holds
G is connected
let G be GraphUnion of G1,G2; :: thesis: ( the_Vertices_of G1 meets the_Vertices_of G2 implies G is connected )

per cases ( G1 tolerates G2 or not G1 tolerates G2 ) ;

suppose A1: G1 tolerates G2 ; :: thesis: ( the_Vertices_of G1 meets the_Vertices_of G2 implies G is connected )

then A2: G is Supergraph of G2 by GLIB_014:26;
assume the_Vertices_of G1 meets the_Vertices_of G2 ; :: thesis: G is connected
then consider u being object such that
A3: ( u in the_Vertices_of G1 & u in the_Vertices_of G2 ) by XBOOLE_0:3;

now :: thesis: for v, w being Vertex of G ex W being Walk of G st W is_Walk_from v,w

let v, w be Vertex of G; :: thesis: ex W being Walk of G st b₃ is_Walk_from W,b₂
the_Vertices_of G = (the_Vertices_of G1) \/ (the_Vertices_of G2) by A1, GLIB_014:25;

per cases then ( ( v in the_Vertices_of G1 & w in the_Vertices_of G1 ) or ( v in the_Vertices_of G1 & w in the_Vertices_of G2 ) or ( v in the_Vertices_of G2 & w in the_Vertices_of G1 ) or ( v in the_Vertices_of G2 & w in the_Vertices_of G2 ) ) by XBOOLE_0:def 3;

suppose ( v in the_Vertices_of G1 & w in the_Vertices_of G1 ) ; :: thesis: ex W being Walk of G st b₃ is_Walk_from W,b₂

then consider W being Walk of G1 such that
A4: W is_Walk_from v,w by GLIB_002:def 1;
reconsider W = W as Walk of G by GLIB_006:75;
take W = W; :: thesis: W is_Walk_from v,w
thus W is_Walk_from v,w by A4, GLIB_001:19; :: thesis: verum

end;

suppose A5: ( v in the_Vertices_of G1 & w in the_Vertices_of G2 ) ; :: thesis: ex W being Walk of G st b₃ is_Walk_from W,b₂

then consider W1 being Walk of G1 such that
A6: W1 is_Walk_from v,u by A3, GLIB_002:def 1;
reconsider W1 = W1 as Walk of G by GLIB_006:75;
consider W2 being Walk of G2 such that
A7: W2 is_Walk_from u,w by A3, A5, GLIB_002:def 1;
reconsider W2 = W2 as Walk of G by A2, GLIB_006:75;
reconsider W = W1 .append W2 as Walk of G ;
take W = W; :: thesis: W is_Walk_from v,w
( W1 is_Walk_from v,u & W2 is_Walk_from u,w ) by A6, A7, GLIB_001:19;
hence W is_Walk_from v,w by GLIB_001:31; :: thesis: verum

end;

suppose A8: ( v in the_Vertices_of G2 & w in the_Vertices_of G1 ) ; :: thesis: ex W being Walk of G st b₃ is_Walk_from W,b₂

then consider W1 being Walk of G2 such that
A9: W1 is_Walk_from v,u by A3, GLIB_002:def 1;
reconsider W1 = W1 as Walk of G by A2, GLIB_006:75;
consider W2 being Walk of G1 such that
A10: W2 is_Walk_from u,w by A3, A8, GLIB_002:def 1;
reconsider W2 = W2 as Walk of G by GLIB_006:75;
reconsider W = W1 .append W2 as Walk of G ;
take W = W; :: thesis: W is_Walk_from v,w
( W1 is_Walk_from v,u & W2 is_Walk_from u,w ) by A9, A10, GLIB_001:19;
hence W is_Walk_from v,w by GLIB_001:31; :: thesis: verum

end;

suppose ( v in the_Vertices_of G2 & w in the_Vertices_of G2 ) ; :: thesis: ex W being Walk of G st b₃ is_Walk_from W,b₂

then consider W being Walk of G2 such that
A11: W is_Walk_from v,w by GLIB_002:def 1;
reconsider W = W as Walk of G by A2, GLIB_006:75;
take W = W; :: thesis: W is_Walk_from v,w
thus W is_Walk_from v,w by A11, GLIB_001:19; :: thesis: verum

end;

end;

end;

hence G is connected by GLIB_002:def 1; :: thesis: verum

end;

suppose not G1 tolerates G2 ; :: thesis: ( the_Vertices_of G1 meets the_Vertices_of G2 implies G is connected )

then G1 == G by GLIB_014:def 26;
hence ( the_Vertices_of G1 meets the_Vertices_of G2 implies G is connected ) by GLIB_002:8; :: thesis: verum

end;

end;