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 holds Union the Sorts of T = union { (T height<= i) where i is Nat : verum }