let G be _Graph; :: thesis: for W being Walk of G
for m, n being Nat holds len (W .cut m,n) <= len W
let W be Walk of G; :: thesis: for m, n being Nat holds len (W .cut m,n) <= len W
let m, n be Nat; :: thesis: len (W .cut m,n) <= len W
reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 13;

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

suppose ( not m is even & not n is even & m <= n & n <= len W ) ; :: thesis: len (W .cut m,n) <= len W

then W .cut m,n = m,n -cut W by GLIB_001:def 11;
then len (W .cut m9,n9) <= len W by MSSCYC_1:8;
hence len (W .cut m,n) <= len W ; :: thesis: verum

end;

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

hence len (W .cut m,n) <= len W by GLIB_001:def 11; :: thesis: verum

end;

end;