:: deftheorem Def4 defines Polish-WFF-set POLNOT_2:def 4 :
for B being Polish-arity-function
for b₂ being Polish-language of (dom B) holds
( b₂ = Polish-WFF-set B iff ex T being Polish-language ex A being Polish-arity-function of T st
( A = B & b₂ = Polish-WFF-set (T,A) ) );