theorem Th14: :: OSAFREE:14

for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for x being set holds
( x is Element of (ParsedTermsOSA X) iff x is Element of TS (DTConOSA X) )