theorem :: GLIB_006:77

for G being _Graph
for V being set
for G1, G2 being addVertices of G,V holds G1 == G2