:: deftheorem Def21 defines Polish-unOp POLNOT_1:def 27 :
for T being Polish-language
for A being Polish-arity-function of T
for t being Element of T st A . t = 1 holds
Polish-unOp (T,A,t) = Polish-operation (T,A,t);