for P being FinSequence-membered set
for A being Function of P,NAT
for Q being FinSequence-membered set st Q is A -closed holds
Polish-atoms (P,A) c= Q