now

per cases ( ( not m is even & not n is even & m <= n & n <= len W & W . m = W . n ) or m is even or n is even or not m <= n or not n <= len W or not W . m = W . n ) ;

suppose ( not m is even & not n is even & m <= n & n <= len W & W . m = W . n ) ; :: thesis: W .remove m,n is directed

then W .remove m,n = (W .cut 1,m) .append (W .cut n,(len W)) by Def12;
hence W .remove m,n is directed ; :: thesis: verum

end;

suppose ( m is even or n is even or not m <= n or not n <= len W or not W . m = W . n ) ; :: thesis: W .remove m,n is directed

hence W .remove m,n is directed by Def12; :: thesis: verum

end;

end;

end;

hence W .remove m,n is directed ; :: thesis: verum