:: deftheorem Def8 defines primenumber NEWTON:def 8 :
for n being Nat
for b₂ being prime Element of NAT holds
( b₂ = primenumber n iff n = card (SetPrimenumber b₂) );