theorem Th37: :: GLIB_008:37

for G1 being _Graph
for e being set
for G2 being removeEdge of G1,e st e in the_Edges_of G1 holds
G1 is addEdge of G2,(the_Source_of G1) . e,e,(the_Target_of G1) . e