reconsider GG = G as [Weighted] [VLabeled] Subgraph of G by GLIB_000:43;
take GG ; :: thesis: ( GG is weight-inheriting & GG is vlabel-inheriting )
dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def 4;
then the_Weight_of G = (the_Weight_of G) | (the_Edges_of G) by RELAT_1:98;
hence GG is weight-inheriting by Def10; :: thesis: GG is vlabel-inheriting
dom (the_VLabel_of G) c= the_Vertices_of G by Lm2;
then the_VLabel_of GG = (the_VLabel_of G) | (the_Vertices_of G) by RELAT_1:97;
hence GG is vlabel-inheriting by Def12; :: thesis: verum