:: deftheorem defines Polish-ext-domain POLNOT_2:def 14 :
for B being Polish-arity-function
for J being Polish-ext-set of B holds Polish-ext-domain (B,J) = (dom B) \/ (Polish-ext-complement (B,J));