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 INT_1:18, XXREAL_0:2;
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:17;
hence (W .cut 1,lenW2) .addEdge (W . (lenW2 + 1)) = W .cut 1,(lenW2 + 2) by Th42, HEYTING3:1, JORDAN12:3
.= W by Lm18 ;
:: thesis: verum