theorem :: PZFMISC1:8

for I being set
for x being ManySortedSet of I holds x in {x}