theorem :: GLIB_003:21
for G being real-weighted WGraph
for W being Walk of G st W is trivial holds
W .cost() = 0 by Th12, RVSUM_1:72;