theorem :: GLIB_003:29

for G being nonnegative-weighted WGraph
for W being Walk of G holds 0 <= W .cost()