let V, U be set ; :: thesis: 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
let W be Function; :: thesis: 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
let G be finite Graph; :: thesis: 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
let P be oriented Chain of G; :: thesis: 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
let v1, v2 be Element of G; :: thesis: ( 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) ) implies P is_shortestpath_of v1,v2,U,W )
assume that
A1: W is_weight>=0of G and
A2: P is_shortestpath_of v1,v2,V,W and
A3: v1 <> v2 and
A4: V c= U and
A5: 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) ; :: thesis: P is_shortestpath_of v1,v2,U,W
P is_shortestpath_of v1,v2,W by A1, A2, A3, A5, Th61;
then A6: for q being oriented Chain of G st q is_orientedpath_of v1,v2,U holds
cost (P,W) <= cost (q,W) ;
P is_orientedpath_of v1,v2,V by A2;
then P is_orientedpath_of v1,v2,U by A4, Th30;
hence P is_shortestpath_of v1,v2,U,W by A6; :: thesis: verum