theorem :: GLIBPRE0:57

for G2 being _Graph
for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st not v in the_Vertices_of G2 & v1 = v2 & v2 in V holds
( v1 .allNeighbors() = (v2 .allNeighbors()) \/ {v} & v1 .degree() = (v2 .degree()) +` 1 )