theorem Th43: :: PBOOLE:43

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