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 Th28;
hence 0 <= W .cost() by RVSUM_1:84; :: thesis: verum