theorem Th8: :: POLNOT_2:4

for B being Polish-arity-function
for J being Polish-ext-set of B holds Polish-WFF-set B c= J