theorem Th24: :: GLIB_012:24

for G3 being _Graph
for V1, V2 being Subset of (the_Vertices_of G3)
for G1 being addLoops of G3,V1 \/ V2 st V1 misses V2 holds
ex G2 being addLoops of G3,V1 st G1 is addLoops of G2,V2