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 ;
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