let G be _Graph; :: thesis: for W being Walk of G st not 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 )

let W be Walk of G; :: thesis: ( not W is trivial implies ex lenW2 being odd Element of NAT st
( lenW2 = (len W) - 2 & (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W ) )

set lenW2 = (len W) - (2 * 1);
assume not W is trivial ; :: thesis: ex lenW2 being odd Element of NAT st
( lenW2 = (len W) - 2 & (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W )

then len W >= 3 by Lm54;
then reconsider lenW2 = (len W) - (2 * 1) as odd Element of NAT by ;
set W1 = W .cut (1,lenW2);
set e = W . (lenW2 + 1);
take lenW2 ; :: thesis: ( lenW2 = (len W) - 2 & (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W )
thus lenW2 = (len W) - 2 ; :: thesis: (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W
lenW2 < (len W) - 0 by XREAL_1:15;
hence (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W .cut (1,(lenW2 + 2)) by
.= W by Lm18 ;
:: thesis: verum