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
A6: P is_shortestpath_of v1,v2,W by A1, A2, A3, A5, Th67;

A7: 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 A6, Def17; :: thesis: verum

end;

P is_orientedpath_of v1,v2,V by A2, Def18;
then P is_orientedpath_of v1,v2,U by A4, Th36;
hence P is_shortestpath_of v1,v2,U,W by A7, Def18; :: thesis: verum