theorem :: PBOOLE:83

for I being set
for X, Y being ManySortedSet of I holds X (\) Y c= X (\+\) Y by Th14;