theorem Th72: :: PBOOLE:72

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