theorem :: CLOSURE1:14

for I being set
for A being ManySortedSet of I holds id (bool A) is idempotent MSSetOp of A