theorem :: GLIB_003:10

for G1, G2 being WGraph
for G3 being WSubgraph of G1 st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds
G3 is WSubgraph of G2