Polish-expression-hierarchy (T,A,n) is T -headed by Th66;
then F is T -headed ;
hence T -head F is Element of T by Def22; :: thesis: verum