theorem :: PBOOLE:79

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