theorem Th44: :: OSAFREE:44

for S being monotone regular locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) holds [t,((PTMin X) . t)] in R . (LeastSort t)