set s = the SortSymbol of S;
set x = the Element of X . the SortSymbol of S;
( height ( the Element of X . the SortSymbol of S -term) = 0 & 0 <= i & the Element of X . the SortSymbol of S -term in T ) by Th24, TREES_1:42;
then the Element of X . the SortSymbol of S -term in { t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } ;
hence not T height<= i is empty ; :: thesis: verum