:: deftheorem SORT defines the_sort_of MSAFREE5:def 11 :
for S being non empty non void ManySortedSign
for A being non empty MSAlgebra over S st A is disjoint_valued holds
for a being Element of A
for b₄ being SortSymbol of S holds
( b₄ = the_sort_of a iff a in the Sorts of A . b₄ );