:: deftheorem Def7 defines Polish-atoms POLNOT_1:def 7 :
for P being FinSequence-membered set
for A being Function of P,NAT
for b₃ being Subset of (P *) holds
( b₃ = Polish-atoms (P,A) iff for a being object holds
( a in b₃ iff ( a in P & A . a = 0 ) ) );