theorem Th23: :: OSAFREE:23

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for x, y, s being object st [x,s] in (PTClasses X) . y holds
( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )