theorem :: GLIB_004:40

for G1, G2 being _finite connected real-weighted WGraph
for G3 being WSubgraph of G1 st G3 is minimumSpanningTree of G1 & G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds
G3 is minimumSpanningTree of G2