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