theorem :: CLOSURE2:29

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