for G2 being _finite _Graph
for v being object
for V being finite set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .size() = (G2 .size()) + (card V)