:: deftheorem Def6 defines SetPrimes NEWTON:def 6 :
for b₁ being Subset of NAT holds
( b₁ = SetPrimes iff for n being Nat holds
( n in b₁ iff n is prime ) );