theorem Th31: :: PBOOLE:31

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