let T be Polish-language; :: thesis: T is full Polish-language of T
set A = the empty-yielding Polish-arity-function of T;
T = Polish-WFF-set (T, the empty-yielding Polish-arity-function of T) by Lm9;
hence T is full Polish-language of T ; :: thesis: verum