let V be set ; :: thesis: for W being Function
for G being Graph
for v1, v2 being Element of G
for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) 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 W be Function; :: thesis: for G being Graph
for v1, v2 being Element of G
for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) 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 G
for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) 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 G; :: thesis: for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) 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,V) 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) ) ) )
deffunc H₁( Element of D) -> Real = cost ($1,W);
consider x being Element of D such that
A1: for y being Element of D holds H₁(x) <= H₁(y) from PRE_CIRC:sch 5();
assume D = AcyclicPaths (v1,v2,V) ; :: 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) ) )
then x in AcyclicPaths (v1,v2,V) ;
then consider p being oriented Simple Chain of G such that
A2: x = p and
p is_acyclicpath_of v1,v2,V ;
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 A2; :: 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 A1;
hence cost (p,W) <= cost (pe,W) by A2; :: thesis: verum