theorem Th45: :: OSAFREE:45

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 holds PTCongruence X c= R