theorem Th43: :: OSAFREE:43

for S being monotone regular locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for t1 being Element of TS (DTConOSA X) holds (PTMin X) . ((PTMin X) . t1) = (PTMin X) . t1