:: deftheorem Def1 defines 4k+3_Primes NUMBER05:def 1 :
for b₁ being Subset of NAT holds
( b₁ = 4k+3_Primes iff for n being Nat holds
( n in b₁ iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) ) );