theorem :: PBOOLE:45

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