theorem Th10: :: GLIB_004:10

for G1 being finite real-weighted WGraph
for e being set
for G2 being [Weighted] weight-inheriting removeEdge of G1,e st e in the_Edges_of G1 holds
G1 .cost() = (G2 .cost()) + ((the_Weight_of G1) . e)