let m, n be Nat; :: thesis: seq (m,n) misses {((m + n) + 1),((m + n) + 2)}
assume seq (m,n) meets {((m + n) + 1),((m + n) + 2)} ; :: thesis: contradiction
then consider x being object such that
A1: x in seq (m,n) and
A2: x in {((m + n) + 1),((m + n) + 2)} by XBOOLE_0:3;
consider k being Element of NAT such that
A3: x = k and
1 + m <= k and
A4: k <= m + n by A1;

per cases ( x = (m + n) + 1 or x = (m + n) + 2 ) by A2, TARSKI:def 2;

suppose x = (m + n) + 1 ; :: thesis: contradiction

then (m + n) + 1 <= (m + n) + 0 by A3, A4;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

suppose x = (m + n) + 2 ; :: thesis: contradiction

then (m + n) + 2 <= (m + n) + 0 by A3, A4;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

end;