:: deftheorem Def23 defines Polish-ext-arity POLNOT_2:def 17 :
for B being Polish-arity-function
for J being Polish-ext-set of B
for b₃ being Polish-arity-function of Polish-ext-domain (B,J) holds
( b₃ = Polish-ext-arity (B,J) iff J = Polish-WFF-set ((Polish-ext-domain (B,J)),b₃) );