reconsider GG = G as [Weighted] Subgraph of G by GLIB_000:40;
take GG ; :: thesis: GG is weight-inheriting
thus GG is weight-inheriting ; :: thesis: verum