theorem Th8: :: PBOOLE:8

for I being set
for x, X, Y being ManySortedSet of I holds
( x in X (/\) Y iff ( x in X & x in Y ) )