for W being Function
for G being Graph
for pe being FinSequence of the carrier' of G
for p being oriented Chain of G st pe in AcyclicPaths p & W is_weight>=0of G holds
cost (pe,W) <= cost (p,W)