theorem Th34: :: GLIB_007:34

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .edgesInto {v} = V --> (the_Edges_of G2)