let T be Polish-language; :: thesis: for A being Polish-arity-function of T st A is empty-yielding holds
Polish-WFF-set (T,A) = T
let A be Polish-arity-function of T; :: thesis: ( A is empty-yielding implies Polish-WFF-set (T,A) = T )
assume A1: A is empty-yielding ; :: thesis: Polish-WFF-set (T,A) = T
A2: Polish-WFF-set (T,A) c= T

proof

set Q = Polish-expression-set (T,A);
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Polish-WFF-set (T,A) or a in T )
assume a in Polish-WFF-set (T,A) ; :: thesis: a in T
then reconsider t = a as Element of Polish-expression-set (T,A) ;
consider n being Nat, p, q being FinSequence such that
A5: p in T and
A6: n = A . p and
A7: q in (Polish-expression-set (T,A)) ^^ n and
A8: t = p ^ q by POLNOT_1:32;
n = 0 by A1, A6;
then q in {{}} by A7, POLNOT_1:6;
then q = {} by TARSKI:def 1;
hence a in T by A5, A8, FINSEQ_1:34; :: thesis: verum

end;

T c= Polish-WFF-set (T,A)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in T or a in Polish-WFF-set (T,A) )
assume A10: a in T ; :: thesis: a in Polish-WFF-set (T,A)
A . a = 0 by A1;
then a in Polish-atoms (T,A) by A10, POLNOT_1:def 7;
hence a in Polish-WFF-set (T,A) by POLNOT_1:34, TARSKI:def 3; :: thesis: verum

end;

hence Polish-WFF-set (T,A) = T by A2; :: thesis: verum