theorem :: POLNOT_1:69

for T being Polish-language
for A being Polish-arity-function of T
for F being Polish-WFF of T,A st T -head F in Polish-atoms (T,A) holds
F = T -head F