theorem Th120: :: ABCMIZ_1:120

for S being non void Signature
for X being ManySortedSet of the carrier of S st X is with_missing_variables holds
( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) )