theorem Th22: :: OSAFREE:22

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