theorem Th29: :: PBOOLE:29

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