theorem :: GLIB_007:62

for G3 being _Graph
for v being object
for V being set
for v1 being Vertex of G3
for e being object
for G2 being addAdjVertexAll of G3,v,V st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V & not e in the_Edges_of G2 holds
for G1 being _Graph st ( G1 is addEdge of G2,v1,e,v or G1 is addEdge of G2,v,e,v1 ) holds
G1 is addAdjVertexAll of G3,v,V \/ {v1}