theorem Th25: :: GLIB_012:25

for G2 being loopless _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V holds
( the_Edges_of G2 misses G1 .loops() & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .loops()) )