theorem Th9: :: CLOSURE2:9

for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E (/\) T in Bool M