theorem :: GLIB_006:79

for G1, G2 being _Graph
for V being set st G1 == G2 & V c= the_Vertices_of G2 holds
G1 is addVertices of G2,V