theorem :: PZFMISC1:28

for I being set
for x being ManySortedSet of I holds bool {x} = {(EmptyMS I),{x}}