for S being locally_directed OrderSortedSign
for U1 being non-empty OSAlgebra of S
for E being MSEquivalence-like OrderSortedRelation of U1
for s being Element of S
for x, y being Element of the Sorts of U1 . s holds
( OSClass (E,x) = OSClass (E,y) iff [x,y] in E . s )