theorem :: GLIB_003:30

for G being nonnegative-weighted WGraph
for W1 being Walk of G
for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost()