for W being Function
for G being finite Graph
for v1, v2 being Element of G st AcyclicPaths (v1,v2) <> {} holds
ex pe being FinSequence of the carrier' of G st
( pe in AcyclicPaths (v1,v2) & ( for qe being FinSequence of the carrier' of G st qe in AcyclicPaths (v1,v2) holds
cost (pe,W) <= cost (qe,W) ) ) by Th50;