let n1, m1, n2, m2 be Nat; :: thesis: ( n1 + m1 <= n2 implies primeNumbers (n1,m1) misses primeNumbers (n2,m2) )
assume A1: n1 + m1 <= n2 ; :: thesis: primeNumbers (n1,m1) misses primeNumbers (n2,m2)
( primeNumbers (n1,m1) = (seq (n1,m1)) /\ SetPrimes & primeNumbers (n2,m2) = (seq (n2,m2)) /\ SetPrimes ) by NUMBER14:def 17;
hence primeNumbers (n1,m1) misses primeNumbers (n2,m2) by A1, Th75, XBOOLE_1:76; :: thesis: verum