theorem Th58: :: GLIB_007:58

for G2 being _Graph
for v being object
for V, E being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E holds
E = G1 .edgesBetween (V,{v})