:: deftheorem defines Polish-WFF-set POLNOT_1:def 25 :
for T being Polish-language
for A being Polish-arity-function of T holds Polish-WFF-set (T,A) = Polish-expression-set (T,A);