:: deftheorem Def5 defines the_sort_of MSATERM:def 5 :
for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for t being Term of S,V
for b₄ being SortSymbol of S holds
( b₄ = the_sort_of t iff t in FreeSort (V,b₄) );