theorem
for
e,
V being
set for
W being
Function for
G being
oriented finite Graph for
P,
Q,
R being
oriented Chain of
G for
v1,
v2,
v3 being
Element of
G st
e in the
carrier' of
G &
W is_weight>=0of G &
len P >= 1 &
P is_shortestpath_of v1,
v2,
V,
W &
v1 <> v2 &
v1 <> v3 &
R = P ^ <*e*> &
Q is_shortestpath_of v1,
v3,
V,
W &
e orientedly_joins v2,
v3 &
P islongestInShortestpath V,
v1,
W holds
( (
cost (
Q,
W)
<= cost (
R,
W) implies
Q is_shortestpath_of v1,
v3,
V \/ {v2},
W ) & (
cost (
Q,
W)
>= cost (
R,
W) implies
R is_shortestpath_of v1,
v3,
V \/ {v2},
W ) )