theorem :: GLIB_001:25

for G being _Graph
for W being Walk of G
for n being Element of NAT st n in dom (W .reverse()) holds
( (W .reverse()) . n = W . (((len W) - n) + 1) & ((len W) - n) + 1 in dom W ) by Lm8;