theorem Th24: :: POLNOT_1:24

for P being FinSequence-membered set
for A being Function of P,NAT
for n being Nat holds Polish-expression-hierarchy (P,A,n) c= Polish-expression-hierarchy (P,A,(n + 1))