theorem Th42: :: OSAFREE:42

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