theorem Th32: :: PBOOLE:32
for I being set
for X, Y, Z being ManySortedSet of I holds X (/\) (Y (\/) Z) = (X (/\) Y) (\/) (X (/\) Z)