theorem :: GLIBPRE1:34

for G being _Graph
for W being Walk of G holds W .length() = (W .reverse()) .length()