for W being Function
for G being Graph st W is_weight>=0of G holds
W is_weight_of G by FUNCT_2:7;