theorem Th38: :: GLIB_008:38

for G1 being non _trivial _Graph
for v being Vertex of G1
for e being object
for G2 being removeVertex of G1,v st {e} = v .edgesInOut() & not e Joins v,v,G1 & G1 is not addAdjVertex of G2,v .adj e,e,v holds
G1 is addAdjVertex of G2,v,e,v .adj e