theorem :: PBOOLE:61

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