theorem :: POLNOT_1:36

for P being FinSequence-membered set
for A being Function of P,NAT holds Polish-atoms (P,A) c= Polish-expression-set (P,A) by Th34;