theorem Th27: :: POLNOT_1:27

for P being FinSequence-membered set
for A being Function of P,NAT
for n being Nat
for q being FinSequence st q in (Polish-expression-set (P,A)) ^^ n holds
ex m being Nat st q in (Polish-expression-hierarchy (P,A,m)) ^^ n