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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 A1: ( 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 the carrier 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
then P is_orientedpath_of v1,v2,V by Def18;
then A2: P is_orientedpath_of v1,v2,U by A1, Th36;
A3: P is_shortestpath_of v1,v2,W by A1, Th67;

now

let q be oriented Chain of G; :: thesis: ( q is_orientedpath_of v1,v2,U implies cost P,W <= cost q,W )
assume q is_orientedpath_of v1,v2,U ; :: thesis: cost P,W <= cost q,W
then q is_orientedpath_of v1,v2 by Def4;
hence cost P,W <= cost q,W by A3, Def17; :: thesis: verum

end;

hence P is_shortestpath_of v1,v2,U,W by A2, Def18; :: thesis: verum