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;

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

end;

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;then len (W .cut (m9,n9)) <= len W by MSSCYC_1:8;

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