set W2 = W .cut m,n;

now

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 A1: ( not m is even & not n is even & m <= n & n <= len W ) ; :: thesis: W .cut m,n is trivial

then A2: 1 <= n by HEYTING3:1;
n <= 1 by A1, Lm55;
then A3: n = 1 by A2, XXREAL_0:1;
A4: 1 <= m by A1, HEYTING3:1;
(len (W .cut m,n)) + m = n + 1 by A1, Lm15;
then (len (W .cut m,n)) + 1 = 1 + 1 by A1, A4, A3, XXREAL_0:1;
hence W .cut m,n is trivial by Lm55; :: thesis: verum

end;

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

hence W .cut m,n is trivial by Def11; :: thesis: verum

end;

end;

end;

hence W .cut m,n is trivial ; :: thesis: verum