theorem :: POLNOT_2:18

for K being non trivial Polish-language
for E being Polish-arity-function of K
for e being Element of K
for M being Extension of (Polish-WFF-set (K,E))
for F being Formula of M st E . e = 1 & Polish-ext-head F = e holds
ex G being Formula of M st F = (Polish-unOp (K,M,e)) . G