let G1 be WGraph; :: thesis: for G2 being WSubgraph of G1
for G3 being WSubgraph of G2 holds G3 is WSubgraph of G1
let G2 be WSubgraph of G1; :: thesis: for G3 being WSubgraph of G2 holds G3 is WSubgraph of G1
let G3 be WSubgraph of G2; :: thesis: G3 is WSubgraph of G1
reconsider G39 = G3 as [Weighted] Subgraph of G1 by GLIB_000:43;
the_Weight_of G3 = (the_Weight_of G2) | (the_Edges_of G3) by Def10
.= ((the_Weight_of G1) | (the_Edges_of G2)) | (the_Edges_of G3) by Def10
.= (the_Weight_of G1) | (the_Edges_of G3) by RELAT_1:74 ;
then G39 is weight-inheriting ;
hence G3 is WSubgraph of G1 ; :: thesis: verum