theorem Th16:
for
U,
V being
set for
G being
oriented finite Graph for
P being
oriented Chain of
G for
W being
Function of the
carrier' of
G,
Real>=0 for
v1,
v2 being
Vertex of
G st the
carrier of
G = U \/ V &
v1 in U & ( for
v3,
v4 being
Vertex of
G st
v3 in U &
v4 in V holds
for
e being
set holds
( not
e in the
carrier' of
G or not
e orientedly_joins v3,
v4 ) ) holds
(
P is_shortestpath_of v1,
v2,
U,
W iff
P is_shortestpath_of v1,
v2,
W )