for W being Function
for G being Graph
for pe being FinSequence of the carrier' of G st W is_weight>=0of G holds
cost (pe,W) >= 0