let G1 be addAdjVertex of G,v1,e,v2; :: thesis:

per cases ;

suppose A1: ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis:

for u1, u2 being Vertex of G1 ex W1 being Walk of G1 st W1 is_Walk_from u1,u2

proof

let u1, u2 be Vertex of G1; :: thesis:

per cases ;

suppose u1 in the_Vertices_of G ; :: thesis:

then reconsider w1 = u1 as Vertex of G ;

per cases ;

suppose u2 in the_Vertices_of G ; :: thesis:

then reconsider w2 = u2 as Vertex of G ;
consider W being Walk of G such that
A2: W is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W1 = W as Walk of G1 by Th79;
take W1 ; :: thesis:
thus W1 is_Walk_from u1,u2 by A2, GLIB_001:19; :: thesis:

end;

suppose A3: not u2 in the_Vertices_of G ; :: thesis:

the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} by A1, Def12;
then u2 in {v2} by A3, XBOOLE_0:def 3;
then u2 = v2 by TARSKI:def 1;
then A4: e Joins v1,u2,G1 by A1, Th135;
reconsider w2 = v1 as Vertex of G by A1;
consider W2 being Walk of G such that
A5: W2 is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W = W2 as Walk of G1 by Th79;
W is_Walk_from u1,v1 by A5, GLIB_001:19;
then A6: ( W .first() = u1 & W .last() = v1 ) by GLIB_001:def 23;
set W1 = W .addEdge e;
take W .addEdge e ; :: thesis:
thus W .addEdge e is_Walk_from u1,u2 by A4, A6, GLIB_001:63; :: thesis:

end;

suppose A7: not u1 in the_Vertices_of G ; :: thesis:

A8: the_Vertices_of G1 = (the_Vertices_of G) \/ {v2} by A1, Def12;
then u1 in {v2} by A7, XBOOLE_0:def 3;
then A9: u1 = v2 by TARSKI:def 1;
then e DJoins v1,u1,G1 by A1, Th135;
then A10: e Joins u1,v1,G1 by GLIB_000:16;

per cases ;

suppose u2 in the_Vertices_of G ; :: thesis:

then reconsider w2 = u2 as Vertex of G ;
reconsider w1 = v1 as Vertex of G by A1;
consider W2 being Walk of G such that
A11: W2 is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W = W2 as Walk of G1 by Th79;
W is_Walk_from v1,u2 by A11, GLIB_001:19;
then A12: ( W .first() = v1 & W .last() = u2 ) by GLIB_001:def 23;
set W3 = G1 .walkOf (u1,e,v1);
A13: ( (G1 .walkOf (u1,e,v1)) .first() = u1 & (G1 .walkOf (u1,e,v1)) .last() = v1 ) by A10, GLIB_001:15;
set W1 = (G1 .walkOf (u1,e,v1)) .append W;
take (G1 .walkOf (u1,e,v1)) .append W ; :: thesis:
thus (G1 .walkOf (u1,e,v1)) .append W is_Walk_from u1,u2 by A12, A13, GLIB_001:30; :: thesis:

end;

suppose not u2 in the_Vertices_of G ; :: thesis:

then u2 in {v2} by A8, XBOOLE_0:def 3;
then u2 = u1 by TARSKI:def 1, A9;
then A14: G1 .walkOf u1 is_Walk_from u1,u2 by GLIB_001:13;
take G1 .walkOf u1 ; :: thesis:
thus G1 .walkOf u1 is_Walk_from u1,u2 by A14; :: thesis:

end;

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

end;

suppose A15: ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) ; :: thesis:

for u1, u2 being Vertex of G1 ex W1 being Walk of G1 st W1 is_Walk_from u1,u2

proof

let u1, u2 be Vertex of G1; :: thesis:

per cases ;

suppose u1 in the_Vertices_of G ; :: thesis:

then reconsider w1 = u1 as Vertex of G ;

per cases ;

suppose u2 in the_Vertices_of G ; :: thesis:

then reconsider w2 = u2 as Vertex of G ;
consider W being Walk of G such that
A16: W is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W1 = W as Walk of G1 by Th79;
take W1 ; :: thesis:
thus W1 is_Walk_from u1,u2 by A16, GLIB_001:19; :: thesis:

end;

suppose A17: not u2 in the_Vertices_of G ; :: thesis:

the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} by A15, Def12;
then u2 in {v1} by A17, XBOOLE_0:def 3;
then u2 = v1 by TARSKI:def 1;
then e DJoins u2,v2,G1 by A15, Th136;
then A18: e Joins v2,u2,G1 by GLIB_000:16;
reconsider w2 = v2 as Vertex of G by A15;
consider W2 being Walk of G such that
A19: W2 is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W = W2 as Walk of G1 by Th79;
W is_Walk_from u1,v2 by A19, GLIB_001:19;
then A20: ( W .first() = u1 & W .last() = v2 ) by GLIB_001:def 23;
set W1 = W .addEdge e;
take W .addEdge e ; :: thesis:
thus W .addEdge e is_Walk_from u1,u2 by A18, A20, GLIB_001:63; :: thesis:

end;

suppose A21: not u1 in the_Vertices_of G ; :: thesis:

A22: the_Vertices_of G1 = (the_Vertices_of G) \/ {v1} by A15, Def12;
then u1 in {v1} by A21, XBOOLE_0:def 3;
then A23: u1 = v1 by TARSKI:def 1;
then A24: e Joins u1,v2,G1 by A15, Th136;

per cases ;

suppose u2 in the_Vertices_of G ; :: thesis:

then reconsider w2 = u2 as Vertex of G ;
reconsider w1 = v2 as Vertex of G by A15;
consider W2 being Walk of G such that
A25: W2 is_Walk_from w1,w2 by GLIB_002:def 1;
reconsider W = W2 as Walk of G1 by Th79;
W is_Walk_from v2,u2 by A25, GLIB_001:19;
then A26: ( W .first() = v2 & W .last() = u2 ) by GLIB_001:def 23;
set W3 = G1 .walkOf (u1,e,v2);
A27: ( (G1 .walkOf (u1,e,v2)) .first() = u1 & (G1 .walkOf (u1,e,v2)) .last() = v2 ) by A24, GLIB_001:15;
set W1 = (G1 .walkOf (u1,e,v2)) .append W;
take (G1 .walkOf (u1,e,v2)) .append W ; :: thesis:
thus (G1 .walkOf (u1,e,v2)) .append W is_Walk_from u1,u2 by A26, A27, GLIB_001:30; :: thesis:

end;

suppose not u2 in the_Vertices_of G ; :: thesis:

then u2 in {v1} by A22, XBOOLE_0:def 3;
then u2 = u1 by TARSKI:def 1, A23;
then A28: G1 .walkOf u1 is_Walk_from u1,u2 by GLIB_001:13;
take G1 .walkOf u1 ; :: thesis:
thus G1 .walkOf u1 is_Walk_from u1,u2 by A28; :: thesis:

end;

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

end;

suppose ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ) ; :: thesis:

then G1 == G by Def12;
hence G1 is connected by GLIB_002:8; :: thesis:

end;