:: deftheorem defines DTConOSA OSAFREE:def 5 :
for S being OrderSortedSign
for X being ManySortedSet of S holds DTConOSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(OSREL X) #);