let G1 be addAdjVertexAll of G,v,V; :: thesis: G1 is connected

per cases ( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G ) ;

suppose A1: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: G1 is connected

for G3 being Component of G ex w being Vertex of G3 st w in V

proof

let G3 be Component of G; :: thesis: ex w being Vertex of G3 st w in V
set w = the Element of V;
A2: G == G3 by GLIB_006:55;
the Element of V in the_Vertices_of G by A1, TARSKI:def 3;
then reconsider w = the Element of V as Vertex of G3 by A2, GLIB_000:def 34;
take w ; :: thesis: w in V
thus w in V ; :: thesis: verum

end;

hence G1 is connected by A1, Th72; :: thesis: verum

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: G1 is connected

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

end;

end;