now :: thesis: W .remove (m,n) is trivial
per 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 ) ;
suppose ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n ) ; :: thesis: W .remove (m,n) is trivial
then W .remove (m,n) = (W .cut (1,m)) .append (W .cut (n,(len W))) by Def12;
hence W .remove (m,n) is trivial ; :: thesis: verum
end;
suppose ( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) ; :: thesis: W .remove (m,n) is trivial
hence W .remove (m,n) is trivial by Def12; :: thesis: verum
end;
end;
end;
hence W .remove (m,n) is trivial ; :: thesis: verum