theorem Th28: :: PBOOLE:28

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