:: deftheorem defines is_weight_of GRAPH_5:def 14 :
for G being Graph
for W being Function holds
( W is_weight_of G iff W is Function of the carrier' of G,REAL );