theorem Th19: :: POLNOT_1:19

for P being FinSequence-membered set
for A being Function of P,NAT
for U being Subset of (P *) holds Polish-atoms (P,A) c= Polish-expression-layer (P,A,U)