:: deftheorem AS defines -sort MSAFREE5:def 10 :
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for A being non empty MSAlgebra over S
for a being Element of A holds
( a is s -sort iff a in the Sorts of A . s );