theorem Th64: :: PBOOLE:64

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