theorem :: GLIB_006:107

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 & not ( w1 = v1 & w2 = v2 ) holds
( w1 = v2 & w2 = v1 )