theorem Th131: :: GLIB_001:133

for G being _Graph
for W being Walk of G st W is trivial holds
ex lenW2 being odd Element of NAT st
( lenW2 = (len W) - 2 & (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W )