theorem :: PBOOLE:85

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