theorem :: PBOOLE:118

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