let G1, G2 be WGraph; :: thesis: for 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
let G3 be WGraph; :: thesis: ( G1 == G2 & the_Weight_of G1 = the_Weight_of G2 & G1 is WSubgraph of G3 implies G2 is WSubgraph of G3 )
assume A1: ( G1 == G2 & the_Weight_of G1 = the_Weight_of G2 & G1 is WSubgraph of G3 ) ; :: thesis: G2 is WSubgraph of G3
then reconsider G2' = G2 as [Weighted] Subgraph of G3 by GLIB_000:95;
the_Edges_of G1 = the_Edges_of G2 by A1, GLIB_000:def 36;
then the_Weight_of G2 = (the_Weight_of G3) | (the_Edges_of G2) by A1, Def10;
then G2' is weight-inheriting by Def10;
hence G2 is WSubgraph of G3 ; :: thesis: verum