let W be Function; :: thesis: for G being Graph
for v1, v2 being Element of the carrier of G
for D being non empty finite Subset of (the carrier' of G * ) st D = AcyclicPaths v1,v2 holds
ex pe being FinSequence of the carrier' of G st
( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds
cost pe,W <= cost qe,W ) )
let G be Graph; :: thesis: for v1, v2 being Element of the carrier of G
for D being non empty finite Subset of (the carrier' of G * ) st D = AcyclicPaths v1,v2 holds
ex pe being FinSequence of the carrier' of G st
( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds
cost pe,W <= cost qe,W ) )
let v1, v2 be Element of the carrier of G; :: thesis: for D being non empty finite Subset of (the carrier' of G * ) st D = AcyclicPaths v1,v2 holds
ex pe being FinSequence of the carrier' of G st
( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds
cost pe,W <= cost qe,W ) )
let D be non empty finite Subset of (the carrier' of G * ); :: thesis: ( D = AcyclicPaths v1,v2 implies ex pe being FinSequence of the carrier' of G st
( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds
cost pe,W <= cost qe,W ) ) )
assume A1: D = AcyclicPaths v1,v2 ; :: thesis: ex pe being FinSequence of the carrier' of G st
( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds
cost pe,W <= cost qe,W ) )
deffunc H₁( Element of D) -> Real = cost $1,W;
consider x being Element of D such that
A2: for y being Element of D holds H₁(x) <= H₁(y) from GRAPH_5:sch 2();
x in AcyclicPaths v1,v2 by A1;
then consider p being oriented Simple Chain of G such that
A3: ( x = p & p is_acyclicpath_of v1,v2 ) ;
take p ; :: thesis: ( p in D & ( for qe being FinSequence of the carrier' of G st qe in D holds
cost p,W <= cost qe,W ) )
thus p in D by A3; :: thesis: for qe being FinSequence of the carrier' of G st qe in D holds
cost p,W <= cost qe,W
let pe be FinSequence of the carrier' of G; :: thesis: ( pe in D implies cost p,W <= cost pe,W )
assume pe in D ; :: thesis: cost p,W <= cost pe,W
then reconsider y = pe as Element of D ;
H₁(x) <= H₁(y) by A2;
hence cost p,W <= cost pe,W by A3; :: thesis: verum