theorem Th93: :: PBOOLE:93

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