let G be WGraph; :: thesis: ( G is nonnegative-weighted implies G is real-weighted )
assume G is nonnegative-weighted ; :: thesis: G is real-weighted
then rng (the_Weight_of G) c= Real>=0 by Def14;
then rng (the_Weight_of G) c= REAL by XBOOLE_1:1;
then the_Weight_of G is real-valued by VALUED_0:def 3;
hence G is real-weighted by Def13; :: thesis: verum