theorem :: GLIB_007:56

for G2 being _Graph
for v, v1 being object
for G1 being addAdjVertexAll of G2,v,{v1} st v1 in the_Vertices_of G2 & not v in the_Vertices_of G2 holds
ex e being object st
( not e in the_Edges_of G2 & ( G1 is addAdjVertex of G2,v,e,v1 or G1 is addAdjVertex of G2,v1,e,v ) )