let G1, G2 be WGraph; :: thesis: for G3 being WSubgraph of G1 st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds
G3 is WSubgraph of G2
let G3 be WSubgraph of G1; :: thesis: ( G1 == G2 & the_Weight_of G1 = the_Weight_of G2 implies G3 is WSubgraph of G2 )
assume that
A1: G1 == G2 and
A2: the_Weight_of G1 = the_Weight_of G2 ; :: thesis: G3 is WSubgraph of G2
reconsider G39 = G3 as [Weighted] Subgraph of G2 by A1, GLIB_000:91;
the_Weight_of G3 = (the_Weight_of G2) | (the_Edges_of G3) by A2, Def10;
then G39 is WSubgraph of G2 by Def10;
hence G3 is WSubgraph of G2 ; :: thesis: verum