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