theorem :: PZFMISC1:29

for I being set
for A being ManySortedSet of I holds {A} c= bool A