theorem Th67: :: PBOOLE:67

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