theorem Th35: :: OSAFREE:35

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for R1, R2 being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) st R1 c= R2 holds
OSClass (R1,t) c= OSClass (R2,t)