theorem :: MOEBIUS3:41

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