theorem :: CLOSURE2:25

for I being set
for M being ManySortedSet of I holds |:(Bool M):| = bool M