theorem Th3: :: OSAFREE:3

for S being OrderSortedSign
for X being non-empty ManySortedSet of S holds
( NonTerminals (DTConOSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConOSA X) = Union (coprod X) )