let W be Function; :: thesis: for G being Graph st W is_weight>=0of G holds
W is_weight_of G
let G be Graph; :: thesis: ( W is_weight>=0of G implies W is_weight_of G )
assume W is_weight>=0of G ; :: thesis: W is_weight_of G
then W is Function of the carrier' of G,Real>=0 by Def13;
then W is Function of the carrier' of G,REAL by FUNCT_2:7;
hence W is_weight_of G by Def14; :: thesis: verum