:: deftheorem defines primeNumbers NUMBER14:def 17 :
for m, n being Nat holds primeNumbers (m,n) = (seq (m,n)) /\ SetPrimes;