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