:: deftheorem Def7 defines SetPrimenumber NEWTON:def 7 :
for p being natural Number
for b₂ being Subset of NAT holds
( b₂ = SetPrimenumber p iff for q being Nat holds
( q in b₂ iff ( q < p & q is prime ) ) );