theorem Th15: :: GLIB_003:15
for G being WGraph
for W being Walk of G holds (W .reverse()) .weightSeq() = Rev (W .weightSeq())