:: deftheorem defines deg<= MSAFREE5:def 18 :
for S being non empty non void ManySortedSign
for X being non-empty 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 deg<= i = { r where r is Element of T : deg r <= i } ;