for W being Function
for V being set
for G being finite Graph
for P, Q being oriented Chain of G
for v1, v2, v3 being Vertex of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & Q is_shortestpath_of v1,v3,V,W & ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) ) & P islongestInShortestpath V,v1,W holds
Q is_shortestpath_of v1,v3,V \/ {v2},W