theorem Th71: :: POLNOT_1:71

for T being Polish-language
for A being Polish-arity-function of T
for F being Polish-WFF of T,A
for n being Nat st F in Polish-expression-hierarchy (T,A,(n + 1)) holds
rng (Polish-WFF-args F) c= Polish-expression-hierarchy (T,A,n)