:: deftheorem Def10 defines Polish-arity POLNOT_2:def 16 :
for T being Polish-language
for V being full Polish-language of T
for b₃ being Polish-arity-function of T holds
( b₃ = Polish-arity V iff V = Polish-WFF-set (T,b₃) );