theorem
for
V,
U being
set for
W being
Function for
G being
finite Graph for
P being
oriented Chain of
G for
v1,
v2 being
Element of
G st
W is_weight>=0of G &
P is_shortestpath_of v1,
v2,
V,
W &
v1 <> v2 &
V c= U & ( for
Q being
oriented Chain of
G for
v3 being
Element of
G st not
v3 in V &
Q is_shortestpath_of v1,
v3,
V,
W holds
cost (
P,
W)
<= cost (
Q,
W) ) holds
P is_shortestpath_of v1,
v2,
U,
W