theorem :: PBOOLE:51

for I being set
for X, Y being ManySortedSet of I st Y c= X & X (/\) Y = EmptyMS I holds
Y = EmptyMS I by Th23;