:: deftheorem defines Polish-WFF-head POLNOT_1:def 33 :
for T being Polish-language
for A being Polish-arity-function of T
for F being Polish-WFF of T,A holds Polish-WFF-head F = T -head F;