theorem PrimesSet2: :: MOEBIUS3:38

for n being Nat st n + 1 is Prime holds
SetPrimes (n + 1) = (SetPrimes n) \/ {(n + 1)}