:: deftheorem Def1 defines -Terms MSATERM:def 1 :
for S being non empty non void ManySortedSign
for V being ManySortedSet of the carrier of S holds S -Terms V = TS (DTConMSA V);