theorem Th27: :: GLIB_012:27

for G1, G2 being _Graph
for v being Vertex of G2 holds
( G1 is addLoops of G2,{v} iff ex e being object st
( not e in the_Edges_of G2 & G1 is addEdge of G2,v,e,v ) )