theorem :: GLIB_001:77

for G being _Graph
for W being Walk of G
for n being even Element of NAT st 1 <= n & n <= len W holds
( n div 2 in dom (W .edgeSeq()) & W . n = (W .edgeSeq()) . (n div 2) ) by Lm40;