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