theorem :: POLNOT_1:84

for L being non trivial Polish-language
for E being Polish-arity-function of L
for F being Polish-WFF of L,E holds
( F in Polish-atoms (L,E) iff Polish-arity F = 0 )