theorem :: PBOOLE:48

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