theorem Th41: :: OSAFREE:41

for S being monotone regular locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for t, t1 being Element of TS (DTConOSA X) st t1 in OSClass ((PTCongruence X),t) holds
(PTMin X) . t1 = (PTMin X) . t