theorem Th85: :: POLNOT_1:85

for L being non trivial Polish-language
for E being Polish-arity-function of L
for F being Polish-WFF of L,E st F in Polish-atoms (L,E) holds
( Polish-WFF-head F = F & L -head F = F & Polish-WFF-args F = {} )