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

hence
W .remove (m,n) is trivial
; :: thesis: verumper cases
( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) or not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n )
;

end;