let G2 be WSubgraph of G; :: thesis: G2 is nonnegative-weighted
now :: thesis: for x being object st x in rng (the_Weight_of G2) holds
x in Real>=0
let x be object ; :: thesis: ( x in rng (the_Weight_of G2) implies x in Real>=0 )
A1: rng (the_Weight_of G) c= Real>=0 by Def14;
assume x in rng (the_Weight_of G2) ; :: thesis: x in Real>=0
then A2: x in rng ((the_Weight_of G) | (the_Edges_of G2)) by Def10;
rng ((the_Weight_of G) | (the_Edges_of G2)) c= rng (the_Weight_of G) by RELAT_1:70;
then x in rng (the_Weight_of G) by A2;
hence x in Real>=0 by A1; :: thesis: verum
end;
hence rng (the_Weight_of G2) c= Real>=0 by TARSKI:def 3; :: according to GLIB_003:def 14 :: thesis: verum