reconsider GG = G as [Weighted] Subgraph of G by GLIB_000:40;
take GG ; :: thesis: GG is weight-inheriting
dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def 2;
then the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) by RELAT_1:69;
hence GG is weight-inheriting by Def10; :: thesis: verum