let G be _Graph; :: thesis: for W being Walk of G
for m, n being Element of NAT holds len (W .remove (m,n)) <= len W
let W be Walk of G; :: thesis: for m, n being Element of NAT holds len (W .remove (m,n)) <= len W
let m, n be Element of NAT ; :: thesis: len (W .remove (m,n)) <= len W
set W2 = W .remove (m,n);

now :: thesis: len (W .remove (m,n)) <= len W

per cases ( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) or not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) ;

suppose A1: ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) ; :: thesis: len (W .remove (m,n)) <= len W

then (len (W .remove (m,n))) + n = (len W) + m by Lm24;
then ((len (W .remove (m,n))) + n) - n <= ((len W) + m) - m by A1, XREAL_1:13;
hence len (W .remove (m,n)) <= len W ; :: thesis: verum

end;

suppose ( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) ; :: thesis: len (W .remove (m,n)) <= len W

hence len (W .remove (m,n)) <= len W by Def12; :: thesis: verum

end;

end;

end;

hence len (W .remove (m,n)) <= len W ; :: thesis: verum