theorem Th11: :: GLIB_004:11

for G being _finite real-weighted WGraph
for V1 being non empty Subset of (the_Vertices_of G)
for E1 being Subset of (G .edgesBetween V1)
for G1 being inducedWSubgraph of G,V1,E1
for e being set
for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds
(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()