theorem Th30: :: PBOOLE:30

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