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 ;
for y being object st y in rng (the_Weight_of G) holds
y in Real>=0 by GRAPH_5:def 12, A1;
then rng (the_Weight_of G) c= Real>=0 ;
hence G is nonnegative-weighted ; :: thesis: verum