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

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

hence
len (W .remove (m,n)) <= len W
; :: thesis: verumper 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 )
;

end;

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