let G1 be addEdge of G,v1,e,v2; :: thesis: G1 is connected

per cases ( ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G ) or not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ;

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

for u, v being Vertex of G1 ex W being Walk of G1 st W is_Walk_from u,v

proof

let u, v be Vertex of G1; :: thesis: ex W being Walk of G1 st W is_Walk_from u,v
reconsider u1 = u, v1 = v as Vertex of G by A1, Def11;
consider W1 being Walk of G such that
A2: W1 is_Walk_from u1,v1 by GLIB_002:def 1;
G is Subgraph of G1 by Th61;
then reconsider W = W1 as Walk of G1 by GLIB_001:167;
( W1 .first() = u1 & W1 .last() = v1 ) by A2, GLIB_001:def 23;
then ( W .first() = u & W .last() = v ) by GLIB_001:16;
hence ex W being Walk of G1 st W is_Walk_from u,v by GLIB_001:def 23; :: thesis: verum

end;

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

end;

suppose ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) ; :: thesis: G1 is connected

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

end;

end;