:: deftheorem defines height<= MSAFREE5:def 19 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for i being Nat holds T height<= i = { t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } ;