theorem :: GLIB_007:48

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