theorem Th15: :: OSAFREE:15

for S being OrderSortedSign
for X being V2() ManySortedSet of S
for s being Element of S
for x being set st x in the Sorts of (ParsedTermsOSA X) . s holds
x is Element of TS (DTConOSA X)