:: deftheorem defines is_shortestpath_of GRAPH_5:def 17 :
for G being Graph
for v1, v2 being Vertex of G
for p being oriented Chain of G
for W being Function holds
( p is_shortestpath_of v1,v2,W iff ( p is_orientedpath_of v1,v2 & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds
cost (p,W) <= cost (q,W) ) ) );