:: deftheorem defines Polish-WFF-args POLNOT_1:def 40 :
for T being Polish-language
for A being Polish-arity-function of T
for n being Nat
for F being Element of Polish-expression-hierarchy (T,A,(n + 1)) holds Polish-WFF-args F = decomp ((Polish-expression-hierarchy (T,A,n)),(Polish-arity F),((T,A) -tail F));