Polish-WFF-set (T,A) is T -headed by Th65;
then F is T -headed ;
hence T -head F is Element of T by Def22; :: thesis: verum