theorem :: ABCMIZ_1:119

for S being non void Signature
for X, Y being ManySortedSet of the carrier of S st X c= Y holds
the carrier of (DTConMSA X) c= the carrier of (DTConMSA Y) by Th118, XBOOLE_1:9;