theorem Th14: :: OSAFREE:14

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