let G be _Graph; :: thesis: 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 )
let W be Walk of G; :: thesis: ( 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 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