let T be Polish-language; :: thesis: for A being Polish-arity-function of T holds Polish-WFF-set (T,A) is T -headed
let A be Polish-arity-function of T; :: thesis: Polish-WFF-set (T,A) is T -headed
let p be FinSequence; :: according to POLNOT_1:def 21 :: thesis: ( p in Polish-WFF-set (T,A) implies p is T -headed )
assume p in Polish-WFF-set (T,A) ; :: thesis: p is T -headed
then consider n being Nat such that
A3: p in Polish-expression-hierarchy (T,A,(n + 1)) by Th28;
set U = Polish-expression-hierarchy (T,A,n);
p in Polish-expression-layer (T,A,(Polish-expression-hierarchy (T,A,n))) by A3, Th23;
hence p is T -headed by Th21; :: thesis: verum