:: deftheorem defines is_weight>=0of GRAPH_5:def 13 :
for G being Graph
for W being Function holds
( W is_weight>=0of G iff W is Function of the carrier' of G,Real>=0 );