set s = the SortSymbol of S;
set x = the Element of X . the SortSymbol of S;
( deg ( 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, Th21;
then reconsider r = the Element of X . the SortSymbol of S -term as Element of T ;
( deg r = deg (@ r) & deg (@ r) = 0 & 0 <= i ) by Th21;
then the Element of X . the SortSymbol of S -term in { r1 where r1 is Element of T : deg r1 <= i } ;
hence not T deg<= i is empty ; :: thesis: verum