:: deftheorem Def10 defines weight-inheriting GLIB_003:def 10 :
for G being WGraph
for G2 being [Weighted] Subgraph of G holds
( G2 is weight-inheriting iff the_Weight_of G2 = (the_Weight_of G) | (the_Edges_of G2) );