theorem :: GLIB_012:20

for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V holds G1 .size() = (G2 .size()) +` (card V)