theorem :: CLOSURE2:28

for I being set
for A being ManySortedSet of I holds id (Bool A) is idempotent SetOp of A