theorem :: GLIB_012:28

for G2 being _Graph
for V being finite Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card V) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G2 ex e being object st
( p . (n + 1) is addEdge of p . n,v,e,v & v in V & not e in the_Edges_of (p . n) ) ) )