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 that
A1: G1 == G2 and
A2: the_Weight_of G1 = the_Weight_of G2 and
A3: G1 is WSubgraph of G3 ; :: thesis: G2 is WSubgraph of G3
reconsider G29 = G2 as [Weighted] Subgraph of G3 by A1, A3, GLIB_000:92;
the_Edges_of G1 = the_Edges_of G2 by A1;
then the_Weight_of G2 = (the_Weight_of G3) | (the_Edges_of G2) by A2, A3, Def10;
then G29 is weight-inheriting ;
hence G2 is WSubgraph of G3 ; :: thesis: verum