let G be nonnegative-weighted WGraph; :: thesis: for W being Walk of G holds 0 <= W .cost()
let W be Walk of G; :: thesis: 0 <= W .cost()
for i being Nat st i in dom (W .weightSeq() ) holds
0 <= (W .weightSeq() ) . i by Th35;
hence 0 <= W .cost() by RVSUM_1:114; :: thesis: verum