theorem :: GLIB_003:11

for G1 being WGraph
for G2 being WSubgraph of G1
for x being set st x in the_Edges_of G2 holds
(the_Weight_of G2) . x = (the_Weight_of G1) . x