for I being non empty set
for M being ManySortedSet of I holds id M is Equivalence_Relation of M