theorem Th77: :: PBOOLE:77

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