theorem Th87: :: PBOOLE:87

for I being set
for X, Y being ManySortedSet of I holds X (\+\) Y = (X (\/) Y) (\) (X (/\) Y)