for I being set
for X being ManySortedSet of I holds X (\+\) X = EmptyMS I by Th52;