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