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:5, 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:15;

hence (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W .cut (1,(lenW2 + 2)) by Th39, ABIAN:12, JORDAN12:2

.= W by Lm18 ;

:: thesis: verum

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:5, 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:15;

hence (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W .cut (1,(lenW2 + 2)) by Th39, ABIAN:12, JORDAN12:2

.= W by Lm18 ;

:: thesis: verum