theorem Th42: :: GLIB_012:42

for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 in V holds
ex e being object st
( e DJoins v1,v1,G1 & not e in the_Edges_of G2 & v1 .edgesIn() = (v2 .edgesIn()) \/ {e} & v1 .edgesOut() = (v2 .edgesOut()) \/ {e} & v1 .edgesInOut() = (v2 .edgesInOut()) \/ {e} )