theorem :: MBOOLEAN:5

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