theorem :: PBOOLE:58

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