theorem Th20: :: POLNOT_1:20

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