theorem Th69: :: PBOOLE:69

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