theorem Th23: :: GLIB_001:24

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