let G1, G2 be connected _Graph; :: thesis:
let G be GraphUnion of G1,G2; :: thesis:

per cases ;

suppose A1: G1 tolerates G2 ; :: thesis:

then A2: G is Supergraph of G2 by GLIB_014:26;
assume the_Vertices_of G1 meets the_Vertices_of G2 ; :: thesis:
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:

let v, w be Vertex of G; :: thesis:
the_Vertices_of G = (the_Vertices_of G1) \/ (the_Vertices_of G2) by A1, GLIB_014:25;

per cases by XBOOLE_0:def 3;

suppose ( v in the_Vertices_of G1 & w in the_Vertices_of G1 ) ; :: thesis:

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:
thus W is_Walk_from v,w by A4, GLIB_001:19; :: thesis:

end;

suppose A5: ( v in the_Vertices_of G1 & w in the_Vertices_of G2 ) ; :: thesis:

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:
( 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:

end;

suppose A8: ( v in the_Vertices_of G2 & w in the_Vertices_of G1 ) ; :: thesis:

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:
( 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:

end;

suppose ( v in the_Vertices_of G2 & w in the_Vertices_of G2 ) ; :: thesis:

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:
thus W is_Walk_from v,w by A11, GLIB_001:19; :: thesis:

end;

end;

end;

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

end;

suppose not G1 tolerates G2 ; :: thesis:

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:

end;

end;