set W2 = W .remove m,n;
A1: len (W .remove m,n) <= len W by Lm26;

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 A2: ( not m is even & not n is even & m <= n & n <= len W & W . m = W . n ) ; :: thesis: W .remove m,n is Trail-like

then reconsider m' = m, n' = n as odd Element of NAT ;

now

given a, b being even Element of NAT such that A3: ( 1 <= a & a < b & b <= len (W .remove m,n) & (W .remove m,n) . a = (W .remove m,n) . b ) ; :: thesis: contradiction
( 1 <= b & a <= len (W .remove m,n) ) by A3, XXREAL_0:2;
then A4: ( a in dom (W .remove m,n) & b in dom (W .remove m,n) ) by A3, FINSEQ_3:27;

now

per cases ( a in Seg m or ( m <= a & a <= len (W .remove m,n) ) ) by A2, A4, Lm34;

suppose a in Seg m ; :: thesis: contradiction

then A5: (W .remove m,n) . a = W . a by A2, Lm29;

now

per cases ( b in Seg m or ( m <= b & b <= len (W .remove m,n) ) ) by A2, A4, Lm34;

suppose b in Seg m ; :: thesis: contradiction

then A6: (W .remove m,n) . b = W . b by A2, Lm29;
b <= len W by A1, A3, XXREAL_0:2;
hence contradiction by A3, A5, A6, Lm57; :: thesis: verum

end;

suppose A7: ( m <= b & b <= len (W .remove m,n) ) ; :: thesis: contradiction

then reconsider b2 = (b - m') + n' as even Element of NAT by A2, Lm30;
A8: ( (W .remove m,n) . b = W . b2 & b2 <= len W ) by A2, A7, Lm30;

now

per cases ( a < b2 or b2 <= a ) ;

suppose a < b2 ; :: thesis: contradiction

hence contradiction by A3, A5, A8, Lm57; :: thesis: verum

end;

suppose b2 <= a ; :: thesis: contradiction

then A9: ((n - m) + b) - b <= a - b by XREAL_1:15;
n - m >= m - m by A2, XREAL_1:15;
then A10: 0 <= a - b by A9;
a - b < b - b by A3, XREAL_1:16;
hence contradiction by A10; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A11: ( m <= a & a <= len (W .remove m,n) ) ; :: thesis: contradiction

then reconsider a2 = (a - m') + n' as even Element of NAT by A2, Lm30;
reconsider nm4 = n' - m' as even Element of NAT by A2, INT_1:18;
A12: ( (W .remove m,n) . a = W . a2 & a2 <= len W ) by A2, A11, Lm30;

now

per cases ( b in Seg m or ( m <= b & b <= len (W .remove m,n) ) ) by A2, A4, Lm34;

suppose b in Seg m ; :: thesis: contradiction

then b <= m by FINSEQ_1:3;
hence contradiction by A3, A11, XXREAL_0:2; :: thesis: verum

end;

suppose A13: ( m <= b & b <= len (W .remove m,n) ) ; :: thesis: contradiction

then reconsider b2 = (b - m') + n' as even Element of NAT by A2, Lm30;
A14: ( (W .remove m,n) . b = W . b2 & b2 <= len W ) by A2, A13, Lm30;

now

per cases ( a2 < b2 or b2 <= a2 ) ;

suppose A15: a2 < b2 ; :: thesis: contradiction

1 <= m' by HEYTING3:1;
then 1 <= a by A11, XXREAL_0:2;
then 1 <= a + nm4 by NAT_1:12;
hence contradiction by A3, A12, A14, A15, Lm57; :: thesis: verum

end;

suppose b2 <= a2 ; :: thesis: contradiction

then b + nm4 <= a + nm4 ;
hence contradiction by A3, XREAL_1:8; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence W .remove m,n is Trail-like by Lm57; :: 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 Trail-like

hence W .remove m,n is Trail-like by Def12; :: thesis: verum

end;

end;

end;

hence W .remove m,n is Trail-like ; :: thesis: verum