for I being set
for X being ManySortedSet of I holds EmptyMS I c= X