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