for P being FinSequence-membered set
for A being Function of P,NAT
for Q being FinSequence-membered set
for n being Nat st Q is A -closed holds
Polish-expression-hierarchy (P,A,n) c= Q