theorem Th65: :: PBOOLE:65

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