theorem :: GLIB_001:53

for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds
(W .cut (1,m)) .last() = (W .cut (n,(len W))) .first() by Lm28;