theorem Th20: :: OSAFREE:20

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for t being Element of TS (DTConOSA X)
for s being Element of S st ex y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds
[t,s] in (PTClasses X) . t