for n being Nat holds not n + 1 in SetPrimes n