theorem :: GLIB_007:31

for G, G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G,v,V st G1 == G2 holds
G2 is addAdjVertexFromAll of G,v,V