theorem :: PBOOLE:117

for I being set
for X, Y being ManySortedSet of I st X (\) Y = X holds
X misses Y