theorem Th15: :: GLIB_012:15

for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds the_Vertices_of G1 = the_Vertices_of G2