theorem Th28: :: POLNOT_1:28

for P being FinSequence-membered set
for A being Function of P,NAT
for a being object st a in Polish-expression-set (P,A) holds
ex n being Nat st a in Polish-expression-hierarchy (P,A,(n + 1))