for V being set
for W being Function
for G being Graph
for v1, v2 being Element of G
for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) holds
ex pe being FinSequence of the carrier' of G st
( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds
cost (pe,W) <= cost (qe,W) ) )