theorem :: MSAFREE5:21

for S being non empty non void ManySortedSign
for A being disjoint_valued non empty MSAlgebra over S
for a being Element of A holds a is the_sort_of a -sort by SORT;