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 P is_orientedpath_of v1,v2 & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,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 P is_orientedpath_of v1,v2 & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W
let P be oriented Chain of G; :: thesis: for v1, v2 being Element of the carrier of G st P is_orientedpath_of v1,v2 & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W
let v1, v2 be Element of the carrier of G; :: thesis: ( P is_orientedpath_of v1,v2 & W is_weight>=0of G implies ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W )
assume A1: ( P is_orientedpath_of v1,v2 & W is_weight>=0of G ) ; :: thesis: ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W
then AcyclicPaths v1,v2 <> {} by Th47;
then consider r being FinSequence of the carrier' of G such that
A2: ( r in AcyclicPaths v1,v2 & ( for s being FinSequence of the carrier' of G st s in AcyclicPaths v1,v2 holds
cost r,W <= cost s,W ) ) by Th56;
consider t being oriented Simple Chain of G such that
A3: ( r = t & t is_acyclicpath_of v1,v2 ) by A2;
take t ; :: thesis: t is_shortestpath_of v1,v2,W
thus t is_orientedpath_of v1,v2 by A3, Def6; :: according to GRAPH_5:def 17 :: thesis: for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds
cost t,W <= cost q,W

hereby :: thesis: verum

let s be oriented Chain of G; :: thesis: ( s is_orientedpath_of v1,v2 implies cost t,W <= cost s,W )
assume A4: s is_orientedpath_of v1,v2 ; :: thesis: cost t,W <= cost s,W
then AcyclicPaths s <> {} by Th47;
then consider x being Element of the carrier' of G * such that
A5: x in AcyclicPaths s by SUBSET_1:10;
A6: cost x,W <= cost s,W by A1, A5, Th60;
AcyclicPaths s c= AcyclicPaths v1,v2 by A4, Th44;
then cost r,W <= cost x,W by A2, A5;
hence cost t,W <= cost s,W by A3, A6, XXREAL_0:2; :: thesis: verum

end;