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