:: deftheorem defines DTConMSA MSAFREE:def 8 :
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds DTConMSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);