for G1 being _Graph
for v being object
for V being Subset of (the_Vertices_of G1)
for G2 being addAdjVertexAll of G1,v,V
for G3 being GraphComplement of G1 st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 holds
ex G4 being addAdjVertexAll of G3,v,(the_Vertices_of G1) \ V st G4 is GraphComplement of G2