for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for w being Vertex of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v = w holds
( w .allNeighbors() = V & w .degree() = card V )