theorem Th51: :: GLIB_007:51

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for E being set
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 holds
( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )