theorem PrimesSet: :: MOEBIUS3:36

for n being Nat st n + 1 is not Prime holds
SetPrimes (n + 1) = SetPrimes n