theorem :: MSAFREE5:61

for i being Nat
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 holds T height<= (i + 1) = (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T))