let G be nonnegative-weighted WGraph; :: thesis: for W1 being Walk of G
for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost()
let W1 be Walk of G; :: thesis: for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost()
let W2 be Subwalk of W1; :: thesis: W2 .cost() <= W1 .cost()
( ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws & ( for i being Element of NAT st i in dom (W1 .weightSeq()) holds
0 <= (W1 .weightSeq()) . i ) ) by Th18, Th28;
hence W2 .cost() <= W1 .cost() by Th2; :: thesis: verum