set W2 = W .cut (m,n);

now :: thesis: W .cut (m,n) is trivial

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

then A2: 1 <= n by ABIAN:12;
n <= 1 by A1, Lm55;
then A3: n = 1 by A2, XXREAL_0:1;
A4: 1 <= m by A1, ABIAN:12;
(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 ( not m is odd or not n is odd 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