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

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

hence
W .cut (m,n) is trivial
; :: thesis: verumper 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 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;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

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

end;

end;