let G be WGraph; :: thesis: ( G is natural-weighted implies G is nonnegative-weighted )
assume G is natural-weighted ; :: thesis: G is nonnegative-weighted
then A1: the_Weight_of G is natural-valued by Def1;

now

let y be set ; :: thesis: ( y in rng (the_Weight_of G) implies y in Real>=0 )
assume A2: y in rng (the_Weight_of G) ; :: thesis: y in Real>=0
rng (the_Weight_of G) c= NAT by A1, VALUED_0:def 6;
then reconsider y9 = y as Element of NAT by A2;
y9 is Real ;
hence y in Real>=0 by GRAPH_5:def 12; :: thesis: verum

end;

then rng (the_Weight_of G) c= Real>=0 by TARSKI:def 3;
hence G is nonnegative-weighted by GLIB_003:def 14; :: thesis: verum