:: deftheorem defines islongestInShortestpath GRAPH_5:def 19 :
for G being Graph
for pe being FinSequence of the carrier' of G
for V being set
for v1 being Vertex of G
for W being Function holds
( pe islongestInShortestpath V,v1,W iff for v being Vertex of G st v in V & v <> v1 holds
ex q being oriented Chain of G st
( q is_shortestpath_of v1,v,V,W & cost (q,W) <= cost (pe,W) ) );