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