let T be Polish-language; 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; for n being Nat holds Polish-expression-hierarchy (T,A,n) is T -headed
let n be Nat; 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 Th35;
Polish-WFF-set (T,A) is T -headed
by Th60;
then
U is T -headed
;
hence
Polish-expression-hierarchy (T,A,n) is T -headed
; verum