theorem :: GLIB_012:18

for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v being Vertex of G1 st v in V holds
v,v are_adjacent