theorem :: CLOSURE2:12

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