let B be Polish-arity-function; :: thesis: for J being Polish-ext-set of B holds Polish-WFF-set B c= J
let J be Polish-ext-set of B; :: thesis: Polish-WFF-set B c= J
set T = dom B;
set V = Polish-WFF-set B;
reconsider A = B as Polish-arity-function of dom B by Th1;
Polish-WFF-set B = Polish-expression-set ((dom B),A) by Def4;
hence Polish-WFF-set B c= J by POLNOT_1:37; :: thesis: verum