for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds
for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class (C1,x) c= Class (C2,y) & ( A is non-empty implies Class (C1,y) c= Class (C2,x) ) )