for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s1, s2 being Element of S
for x being Element of the Sorts of U1 . s1 st s1 <= s2 holds
for y being Element of the Sorts of U1 . s2 st y = x holds
OSClass (E,x) = OSClass (E,y) by Th4;