set A = the Polish-arity-function of T;
take Polish-WFF-set (T, the Polish-arity-function of T) ; :: thesis: Polish-WFF-set (T, the Polish-arity-function of T) is full
thus Polish-WFF-set (T, the Polish-arity-function of T) is full ; :: thesis: verum