let T be Polish-language; :: thesis: for A being Polish-arity-function of T
for n being Nat holds Polish-expression-hierarchy (T,A,n) is T -headed
let A be Polish-arity-function of T; :: thesis: for n being Nat holds Polish-expression-hierarchy (T,A,n) is T -headed
let n be Nat; :: thesis: Polish-expression-hierarchy (T,A,n) is T -headed
reconsider U = Polish-expression-hierarchy (T,A,n) as Subset of (Polish-WFF-set (T,A)) by Th26;
Polish-WFF-set (T,A) is T -headed by Th65;
then U is T -headed ;
hence Polish-expression-hierarchy (T,A,n) is T -headed ; :: thesis: verum