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

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

suppose ( m is odd & n is odd & 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 ( not m is odd or not n is odd 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;