theorem Th72: :: GLIB_007:72

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( for G3 being Component of G2 ex w being Vertex of G3 st w in V ) holds
G1 is connected